Changelog
2024-09-13 00:04 d0afdfd7
chore: fix docstring of `HeytingAlgebra.himp_bot` (#16587) …
1 files
2024-09-12 22:13 56da879c
chore: Move pointwise finset lemmas under `Algebra` (#16744)
16 files
2024-09-12 20:44 0829f931
chore(scripts/get_tlabel.sh): use 'CI' and 'IMO' labels for maintainer merge (#16726)
1 files
2024-09-12 19:09 9c097105
feat(Tactic/CategoryTheory/ToApp): Add `to_app` attribute (#16119) …
9 files3 theorems3 defs
2024-09-12 18:54 e6bff577
feat(Ergodic/Conservative): add `Conservative.measureRestrict` (#16126)
1 files2 theorems
2024-09-12 17:39 2f662a44
chore(LinearAlgebra): prepare library for API refactor (#16738) …
9 files8 theorems
2024-09-12 17:39 718a757c
feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) …
7 files6 theorems1 structures
2024-09-12 16:41 24f01798
chore: match the definition of `AnalyticWithinAt` with `ContDiffWithinAt` (#16725) …
4 files59 theorems
2024-09-12 16:24 862c6652
chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …
4 files50 theorems2 defs
2024-09-12 14:29 185d8006
feat(CategoryTheory/Abelian): AB4 and AB5 axioms (#6504) …
5 files
2024-09-12 10:52 776511a5
feat(CategoryTheory/Filtered): finality and initiality of projections on (co)structured arrow cats (#16680)
1 files
2024-09-12 10:52 0ca9b837
feat: lint on (syntactically) duplicate imports (#16384) …
1 files1 defs
2024-09-12 10:52 dc64441f
feat: Prop-valued version of `RCLike` structure for normed fields (#16383) …
5 files1 theorems
2024-09-12 09:57 2f55b8c9
chore: deprecate 14 `Init.Logic` lemmas (#16721) …
354 files12 theorems
2024-09-12 09:56 97fb6216
chore: split Analysis.ContDiff.Defs into two files (#16720) …
3 files138 theorems4 defs4 structures
2024-09-12 09:29 a7090176
feat(Algebra/OpenSubgroup): quotient of compact group by open subgroup is finite (#16671) …
2 files5 theorems
2024-09-12 09:29 317d5fd9
feat(CategoryTheory/Monoidal): string diagram command (#15929) …
3 files1 defs
2024-09-12 08:50 2c64747c
feat(Data/Nat/Bitwise): more symmetric statement of `Nat.xor_trichotomy` (#16693) …
1 files2 theorems
2024-09-12 08:03 b589cdd6
chore: include LeanSearchClient in the cache (#16717)
1 files
2024-09-12 07:15 002afcff
feat: `Small.{u}` sets are closed under various operations (#11126) …
2 files7 theorems
2024-09-12 06:16 7eb3f52a
feat: generalize Module.Free.ChooseBasisIndex.fintype and Module.Finite.matrix to semirings (#16700)
1 files
2024-09-12 06:16 06a043ee
feat(Combinatorics/Configuration): Projective planes over fields (#16684) …
2 files5 theorems
2024-09-12 06:16 25ed3261
chore: remove some unnecessary `have`s (#16659) …
18 files
2024-09-12 06:16 381b26ac
feat(Order/SuccPred/Limit): `IsSuccLimit` (#16499) …
4 files60 theorems2 defs
2024-09-12 06:16 bb2f2f9f
feat: improve `subst_hom_lift` macro (#16304) …
2 files
2024-09-12 05:45 05bd9c4e
chore(SetTheory/Ordinal/Arithmetic): hide implementation details (#16703) …
2 files4 theorems
2024-09-12 05:45 6bdc3635
feat(SetTheory/Ordinal/Basic): prove linear order instance earlier (#16401) …
2 files3 theorems
2024-09-12 05:36 7e96235b
feat(Algebra/Order/Archimedean/Submonoid): `SubmonoidClass.instMulArchimedean` (#16430)
2 files
2024-09-12 04:36 086be1c4
feat: catch non-zero exit code from print-style-output (#16709) …
1 files
2024-09-12 04:36 40052abb
feat: #leansearch command (#16695) …
3 files
2024-09-12 03:40 d813c097
chore: deprecate all but `IsSymmOp` in `Init.Algebra.Classes` (#16698) …
4 files
2024-09-12 01:45 b9bbf9b8
chore: namespace `rsuffices` (#16708) …
1 files
2024-09-11 20:04 216c7540
chore: update Mathlib dependencies 2024-09-11 (#16714) …
1 files
2024-09-11 18:10 d1657b5f
fix: please the long line linter in check-yaml (#16697) …
1 files1 defs
2024-09-11 15:57 0c868b65
feat(Lie): make `CommutatorRing` a `NonUnitalNonAssocRing` (#16702) …
1 files
2024-09-11 15:57 d6fe193e
feat(Data/Set/Finite): added lemmas about cardinality of finite sets (#15652) …
1 files3 theorems
2024-09-11 15:20 ef7e491a
feat(GroupTheory/GroupAction/Quotient): `equivSubgroupOrbitsQuotientGroup` (#15506) …
1 files
2024-09-11 14:35 5d603d75
feat(Algebra/BigOperators/Associated): add lemma divisor_closure_eq_closure (#11888) …
1 files1 theorems
2024-09-11 12:15 ef71a8c9
feat(Algebra/Polynomial/Derivation): coefficient-wise derivation on a polynomial (#14702) …
2 files7 theorems1 defs
2024-09-11 09:59 53d5e938
fix: make print-style-errors.sh robust against file names with quotes (#16699) …
1 files
2024-09-11 05:42 4b83244f
chore: deprecate `dif_ctx_congr`, move `if_(ctx_)congr` (#16692) …
5 files4 theorems
2024-09-11 04:48 0e1a0b8d
chore: remove variables from LinearAlgebra.FreeModule.Finite.Basic (#16662) …
1 files1 theorems
2024-09-11 04:48 82ae4e3b
feat: MonoidHom.div_mem_ker_iff (#16642)
1 files1 theorems
2024-09-11 04:48 202f4891
feat(Algebra/BigOperators): product of MulHom over nonempty multisets (#16602)
1 files3 theorems
2024-09-11 04:47 d46e3640
feat(FieldTheory/{SeparableDegree|PurelyInseparable}): generalize some results on purely inseparable extension to non-commutative case (#16585) …
2 files8 theorems
2024-09-11 03:54 e992840b
chore: move `ExistsUnique`, `Xor'` out of `Init.Logic` (#16691) …
10 files34 theorems8 defs
2024-09-11 03:54 cb6040d8
feat(ModelTheory/Satisfiability): Fix universe on ModelsBoundedFormula, derive consequences for models in all universes (#16676) …
1 files7 theorems
2024-09-11 03:53 00efa9fd
feat(Filter/Prod): add `comap_prodMap_prod` (#16564)
1 files2 theorems
2024-09-11 03:05 720235a4
Revert "perf: synth order of `SMul` hierarchy (#16646)" (#16689) …
11 files1 defs
2024-09-11 02:46 23123003
chore: make inner product notation `⟪x, y⟫_𝕜` scoped in namespace `InnerProductSpace` (#16672) …
13 files