Zobrazeno 1 - 10
of 351
pro vyhledávání: '"mathlib"'
Autor:
Nash, Oliver
We discuss the theory of Lie algebras in Lean's Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel's theorem and an application to root space theory. We emphasise that all arguments work with coefficients in
Externí odkaz:
http://arxiv.org/abs/2304.10424
Autor:
Ying, Kexing, Degenne, Rémy
We present the formalization of Doob's martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in $L^1$. In order to formalize thos
Externí odkaz:
http://arxiv.org/abs/2212.05578
Autor:
Gouëzel, Sébastien
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive se
Externí odkaz:
http://arxiv.org/abs/2207.12742
Autor:
Wieser, Eric
Publikováno v:
Workshop Papers of the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania, July 26 - 31, 2021, https://ceur-ws.org/Vol-3377/fmm11.pdf
Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses are used by mathlib for scalar actions with examples, illustrate some o
Externí odkaz:
http://arxiv.org/abs/2108.10700
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Kniha
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Sébastien Gouëzel
Publikováno v:
Lecture Notes in Computer Science
15th Conference on Intelligent Computer Mathematics
15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi, Georgia. pp.3-18, ⟨10.1007/978-3-031-16681-5_1⟩
Lecture Notes in Computer Science ISBN: 9783031166808
15th Conference on Intelligent Computer Mathematics
15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi, Georgia. pp.3-18, ⟨10.1007/978-3-031-16681-5_1⟩
Lecture Notes in Computer Science ISBN: 9783031166808
International audience; We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d0e285985931a6fd70da1ee83ce5d09
https://hal.science/hal-03737714/file/samplepaper.pdf
https://hal.science/hal-03737714/file/samplepaper.pdf
Autor:
Oliver Nash
Publikováno v:
Journal of Automated Reasoning. 67
We discuss the theory of Lie algebras in Lean’s Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel’s theorem and an application to root space theory. We emphasise that all arguments work with coefficients
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::81114f7185be10bb9cbd6791b903c0e6
https://doi.org/10.1007/s10817-023-09668-0
https://doi.org/10.1007/s10817-023-09668-0
Conference
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Wieser, E
Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses are used by mathlib for scalar actions with examples, illustrate some o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::afc66714cff618fc3a5bd08fc47f4e10