Changelog

2024-07-14 03:25 81fa779e
feat(LineDeriv/QuadraticMap): new file (#14450) …
3 files2 theorems
2024-07-14 02:03 670cd521
feat(SpecialFunctions.Log.ENNRealLog): remove a coercion in log_pow (#14714) …
2 files1 theorems
2024-07-14 01:52 cdb5bd69
feat(SetTheory/Surreal/Basic): add some lemmas for Surreal.mk (#14600) …
1 files10 theorems
2024-07-14 01:52 2d55389b
fix(SetTheory/Game/Basic): Fix the definition of surreal inverse (#14463) …
1 files1 theorems1 defs
2024-07-14 01:42 711980bd
feat(SetTheory/Game/PGame): inserting an option a game (#14517) …
2 files9 theorems2 defs
2024-07-13 21:21 548ca520
feat(LocalExtr/Basic): add lemmas about `_ ∈ posTangentConeAt _ _` (#14434)
2 files14 theorems
2024-07-13 20:05 79741dbd
feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences (#14482)
2 files4 theorems
2024-07-13 19:14 eed869b6
feat(Order.LiminfLimsup): add limsup_max (#14564) …
3 files18 theorems
2024-07-13 18:48 100eb1d0
feat (RingTheory/HahnSeries) SMulZeroClass instances (#13421) …
2 files5 theorems1 defs
2024-07-13 18:20 dd161e4b
feat(CategoryTheory/GlueData): New constructor for glue data. (#14548)
3 files8 theorems2 defs1 structures
2024-07-13 17:36 98151c27
refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise `QuadraticForm` to `QuadraticMap` (#7569) …
25 files239 theorems47 defs2 structures
2024-07-13 16:27 b4502d4e
feat: make nonZeroDivisors.coe_ne_zero simp (#14637) …
2 files
2024-07-13 15:29 f445d486
feat(RingTheory/TensorProduct/Basic): Lifting linear maps to base change (#14374)
1 files5 theorems1 defs
2024-07-13 13:40 e8606835
refactor: improvements to lint_style (#14676) …
2 files3 defs
2024-07-13 13:40 4ffab454
style(Mathlib/Tactic/Congr!): rename `Congr!.lean` to `CongrExclamation.lean` to avoid the illegal character `!` (#13280) …
8 files
2024-07-13 12:38 433fb11a
chore: remove autoImplicit in Util (#14694) …
8 files1 theorems3 defs
2024-07-13 11:59 0512d468
doc: fix definition names in GCDMonoid.Basic (#14703)
1 files
2024-07-13 09:51 fa54a2cb
chore(Integral/Lebesgue): golf (#14700) …
1 files
2024-07-13 07:32 ce2899f1
feat: a replacement for `Nat.leRecOn'` that works with `induction` (#14431) …
5 files12 theorems4 defs
2024-07-13 02:59 9d09e659
docs(Data/Finset/Basic): fix docstring referring to other files (#14692) …
1 files
2024-07-13 02:59 4bd8d80e
docs: fix references.bib (#14689) …
1 files
2024-07-13 02:04 edcb1f98
chore: remove unused lemmas about bit0/1 (#14678)
2 files10 theorems
2024-07-13 01:16 44a0195d
feat(GroupTheory/GroupAction): Add theorem for `smul` of `toConjAct` (#14673) …
1 files1 theorems
2024-07-13 01:16 8cf527bf
style: fix some double spaces (#14662) …
20 files3 theorems1 defs
2024-07-13 01:16 fb975644
refactor: give `edist_dist` a default value (#14651)
12 files
2024-07-13 00:30 c6a93595
chore(BigOperators/Ring): generalize `Fintype.sum_mul_sum` (#14683) …
1 files1 theorems
2024-07-12 23:56 8e7020a5
feat(MeasureTheory): drop measurability assumptions here and there (#14680)
11 files11 theorems
2024-07-12 22:59 de620253
feat(Decomposition/Lebesgue): `SigmaFinite -> SFinite` (#14658) …
9 files13 theorems
2024-07-12 20:12 e539139d
feat: Translation of affine bases (#14682) …
5 files11 theorems
2024-07-12 17:57 4bbd5e48
chore: update Mathlib dependencies 2024-07-12 (#14681) …
0 files
2024-07-12 17:57 c0af29f6
chore: Move more lemmas to `Algebra.Group.Action.Defs` (#14677) …
3 files16 theorems
2024-07-12 17:08 1968eab9
chore: update Mathlib dependencies 2024-07-12 (#14679) …
1 files
2024-07-12 15:32 d419680b
chore: remove spaces in binders (#14664) …
10 files4 theorems
2024-07-12 14:36 b355a7a3
feat: Lemmas `DifferentiableAt.add_iff_left`, `DifferentiableAt.add_iff_right` (#14593) …
3 files12 theorems
2024-07-12 14:35 6bfe732c
feat(AlgebraicGeometry/PrimeSpectrum): Prime spectrum of products of rings. (#14550)
2 files3 theorems1 defs
2024-07-12 14:35 2f97af5d
feat: basic results about `Finset.sym2` (#14212)
4 files12 theorems2 defs
2024-07-12 14:35 c2057164
feat(SpecialFunctions/Log): Add extended exp (#14107) …
5 files65 theorems3 defs
2024-07-12 14:35 f8516eba
feat: Density of a finset (#11243) …
5 files30 theorems2 defs
2024-07-12 13:34 d9e0e06d
feat(AlgebraicGeometry/Modules/Tilde): construct the tilde sheaf associated to a module (#14231) …
2 files2 theorems7 defs
2024-07-12 13:34 31c0e2a6
feat(LightProfinite): define `ℕ∪{∞}` as a light profinite set (#13358) …
3 files2 theorems
2024-07-12 13:34 12b4bd72
feat(Topology): restriction of a `QuotientMap` (#13228) …
3 files5 theorems
2024-07-12 12:01 2b726f5e
chore: remove `@[simp]` from `List.replicate_succ` (#14527) …
3 files
2024-07-12 11:12 e0d8b5b4
chore: remove unused lemmas about bit0/1 (#14672)
2 files6 theorems
2024-07-12 10:19 fffcdb50
fix: rewrite Int.eq_pow_of_mul_eq_pow_* lemmas in terms of Odd (#14671)
1 files6 theorems
2024-07-12 09:29 8ba988d4
feat(RingTheory/AdicCompletion): comparison with tensor product (#14358) …
5 files8 theorems3 defs
2024-07-12 08:45 f8b05dcd
chore(AEEqOfIntegral): weaken TC assumptions in 2 lemmas (#14668) …
2 files1 theorems
2024-07-12 08:45 e2113ef7
chore: remove superfluous `intro`s (#14614)
10 files
2024-07-12 07:41 855a27b8
chore: move non `@[to_additive]` parts of `Algebra.Order.Monoid` and `Algebra.Order.Group` to a different file (#14667) …
16 files112 theorems4 defs
2024-07-12 06:55 41eb6f94
chore: Move `smooth_barycentric_coord` (#14666) …
4 files2 theorems
2024-07-12 04:44 f742b2ad
fix(maintainer_merge_*.yml): don't require \r in maintainer merge comment (#14663) …
3 files