Changelog

2022-12-06 20:53 07fee0ca
feat(geometry/euclidean/circumcenter): reindexing (#17830) …
1 files3 theorems
2022-12-06 20:53 03c860eb
feat(geometry/euclidean/angle/oriented/affine): angles in pairs of parallel lines (#17829) …
1 files2 theorems
2022-12-06 20:53 0d17cfb6
chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821) …
2 files13 theorems
2022-12-06 20:53 dc9db541
feat(data/nat/log): review/extend API (#17809) …
5 files20 theorems
2022-12-06 20:53 41abcdc0
feat(analysis/convex/between): betweenness in a ring (#17755) …
1 files6 theorems
2022-12-06 20:53 514ff6b4
feat(linear_algebra/affine_space/combination): `congr` lemmas (#17659) …
1 files3 theorems
2022-12-06 20:53 ab845455
feat(linear_algebra/affine_space/finite_dimensional): collinearity and spans of two points (#17635) …
1 files5 theorems
2022-12-06 20:53 2af8cec7
feat(geometry/euclidean/angle/unoriented/affine): collinearity lemma (#17634) …
1 files1 theorems
2022-12-06 20:53 a5abf903
feat(geometry/euclidean/circumcenter): equal circumspheres among cospherical points (#17572) …
1 files4 theorems
2022-12-06 20:53 164690af
feat(analysis/convex/between): more transitivity variants (#17527) …
1 files4 theorems
2022-12-06 19:45 6f11155d
feat(algebra/cubic_discriminant): add nat degree and monic lemmas (#17780) …
1 files21 theorems
2022-12-06 17:02 10ac9529
feat(geometry/euclidean/angle/oriented): base angles of isosceles triangles are acute (#17823) …
2 files4 theorems
2022-12-06 17:02 fa256f00
feat(data/polynomial): irreducibility criteria for (quadratic) monic polynomials (#17664) …
6 files10 theorems1 defs
2022-12-06 17:02 7679be23
feat(dynamics/ergodic/add_circle): ergodicity of zsmul on the additive circle (#17544)
7 files12 theorems
2022-12-06 14:57 62f682c0
feat(topology/algebra/module/strong_topology): strong topology on continuous linear maps is locally convex and T2 (#16794)
2 files4 theorems
2022-12-06 14:57 41e1ab75
feat(topology/uniform_space/equicontinuity): definition and basic properties of [uniform] equicontinuity (#16467)
5 files43 theorems3 defs
2022-12-06 09:40 e753057a
feat(algebra/hom/equiv/basic): Add `to_additive` to `Pi_congr_right` lemmas (#17827) …
1 files
2022-12-06 09:40 10ee5ede
chore(logic/basic): golf a proof (#17807) …
1 files1 theorems
2022-12-06 09:40 8770c841
chore(*): add mathlib4 synchronization comments (#17806) …
9 files
2022-12-06 09:40 b9b2114f
chore(number_theory/padics): fix lemma names and golf (#17798) …
2 files3 theorems
2022-12-06 09:40 d7744511
chore(data/polynomial/derivative): change n to C n (#17795) …
4 files3 theorems
2022-12-06 09:40 631175a8
feat(category_theory/idempotents): universal property of karoubi (#17603)
1 files4 theorems5 defs
2022-12-06 09:40 38375881
feat(linear_algebra/affine_space/independent): `affine.simplex.reindex` (#17566) …
1 files5 theorems1 defs
2022-12-06 09:40 8348e173
feat(linear_algebra/affine_space/affine_subspace): `parallel` and affine spans (#17526) …
1 files4 theorems
2022-12-06 07:17 49605783
feat(set_theory/cardinal): add lemmas about `n : ℕ` and `ℵ₀` (#17490)
1 files4 theorems
2022-12-06 04:12 428acaae
move(algebra/order/monoid/*): relocate `zero_le_one_class` again (#17820) …
5 files36 theorems
2022-12-06 00:34 a95b16cb
chore(data/set/constructions): Make `has_finite_inter` Prop-valued (#17824) …
1 files1 theorems1 defs1 structures
2022-12-05 18:49 77314cca
feat(analysis/special_functions/trigonometric/angle): twice angles adding to `π` (#17822) …
1 files2 theorems
2022-12-05 17:04 6ed79339
feat(combinatorics/quiver/*) `cast` arrows and paths along equalities (#17617) …
3 files24 theorems2 defs
2022-12-05 14:00 97b62c86
feat(order/upper_lower): More `prod` lemmas (#17747) …
2 files40 theorems2 defs
2022-12-05 14:00 b1d911ac
chore(algebra/ring/defs): refactor `is_domain` (#17721) …
24 files5 theorems
2022-12-05 11:06 62ec8656
chore(algebra/big_operators/basic): golf results about bUnion (#17501) …
6 files7 theorems
2022-12-05 09:33 347d2ed1
feat(measure_theory/integrals): integration by parts for algebra-valued functions (#17778) …
3 files6 theorems
2022-12-05 08:18 6959abed
feat(geometry/euclidean/angle/oriented/affine): more collinearity / affine independence lemmas (#17815) …
1 files2 theorems
2022-12-05 08:18 88bca0ce
feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577) …
5 files4 theorems
2022-12-05 08:18 c0dd3fc8
refactor(algebraic_geometry/EllipticCurve): generalise elliptic curves into weierstrass curves (#17220) …
2 files48 theorems24 defs3 structures
2022-12-05 07:05 dd1f8496
feat(algebraic_topology/dold_kan): the inverse functor of the Dold-Kan equivalence (#17607)
3 files9 theorems7 defs
2022-12-05 05:36 f1a2caaf
feat(analysis/special_functions/trigonometric/angle): `to_real` lemmas (#17395) …
1 files16 theorems
2022-12-05 00:55 a50170a8
chore(data/{finset,set}/basic): Align lemmas (#17805) …
47 files13 theorems
2022-12-04 20:02 c982179e
feat(*/sub*/pointwise): lemmas about pointwise scalar actions (#17814)
9 files22 theorems
2022-12-04 20:02 ce613251
chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811) …
1 files
2022-12-04 17:00 9b2660e1
feat(algebra/order/zero_le_one): generalize lemmas (#17465) …
46 files33 theorems
2022-12-04 14:17 cc3c8aa5
feat(group_theory): generalize `normal_map` (#17808)
2 files1 theorems
2022-12-04 14:17 6c5959aa
feat(linear_algebra/affine_space/finite_dimensional): more affine independence / collinearity lemmas (#17643) …
2 files4 theorems
2022-12-04 12:17 1a766f5a
feat(data/real/basic): remove typeclass shortcircuit (#17804) …
1 files
2022-12-04 12:16 4ed0bcae
feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023) …
3 files3 theorems
2022-12-04 09:54 6b766f92
feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492) …
3 files14 theorems
2022-12-03 22:32 dad7ecf9
feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801) …
5 files16 theorems
2022-12-03 22:32 d4ebdc81
chore(algebra/group/conj): move out results about finiteness (#17789)
7 files
2022-12-03 19:18 32e4a38c
fix(scripts/port_comments): deal with files that have no header to insert below (#17797) …
1 files