Commits leanprover-community/mathlib3

feat(linear_algebra/affine_space/independent): `affine.simplex.reindex` (#17566)

jsm28 committed 3 years ago

38375881

feat(linear_algebra/affine_space/affine_subspace): `parallel` and affine spans (#17526)

jsm28 committed 3 years ago

8348e173

feat(set_theory/cardinal): add lemmas about `n : ℕ` and `ℵ₀` (#17490)

urkud committed 3 years ago

49605783

move(algebra/order/monoid/*): relocate `zero_le_one_class` again (#17820)

astrainfinita committed 3 years ago

428acaae

chore(data/set/constructions): Make `has_finite_inter` Prop-valued (#17824)

YaelDillies committed 3 years ago

a95b16cb

feat(analysis/special_functions/trigonometric/angle): twice angles adding to `π` (#17822)

jsm28 committed 3 years ago

77314cca

feat(combinatorics/quiver/*) `cast` arrows and paths along equalities (#17617)

bottine committed 3 years ago

6ed79339

feat(order/upper_lower): More `prod` lemmas (#17747)

YaelDillies committed 3 years ago

97b62c86

chore(algebra/ring/defs): refactor `is_domain` (#17721)

riccardobrasca committed 3 years ago

b1d911ac

chore(algebra/big_operators/basic): golf results about bUnion (#17501)

eric-wieser committed 3 years ago

62ec8656

feat(measure_theory/integrals): integration by parts for algebra-valued functions (#17778)

loefflerd committed 3 years ago

347d2ed1

feat(geometry/euclidean/angle/oriented/affine): more collinearity / affine independence lemmas (#17815)

jsm28 committed 3 years ago

6959abed

feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577)

joelriou committed 3 years ago

88bca0ce

refactor(algebraic_geometry/EllipticCurve): generalise elliptic curves into weierstrass curves (#17220)

Multramate committed 3 years ago

c0dd3fc8

feat(algebraic_topology/dold_kan): the inverse functor of the Dold-Kan equivalence (#17607)

joelriou committed 3 years ago

dd1f8496

feat(analysis/special_functions/trigonometric/angle): `to_real` lemmas (#17395)

jsm28 committed 3 years ago

f1a2caaf

chore(data/{finset,set}/basic): Align lemmas (#17805)

YaelDillies committed 3 years ago

a50170a8

feat(*/sub*/pointwise): lemmas about pointwise scalar actions (#17814)

eric-wieser committed 3 years ago

c982179e

chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811)

adomani committed 3 years ago

ce613251

feat(algebra/order/zero_le_one): generalize lemmas (#17465)

astrainfinita committed 3 years ago

9b2660e1

feat(group_theory): generalize `normal_map` (#17808)

urkud committed 3 years ago

cc3c8aa5

feat(linear_algebra/affine_space/finite_dimensional): more affine independence / collinearity lemmas (#17643)

jsm28 committed 3 years ago

6c5959aa

feat(data/real/basic): remove typeclass shortcircuit (#17804)

hrmacbeth committed 3 years ago

1a766f5a

feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023)

kim-em committed 3 years ago

4ed0bcae

feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492)

kkytola committed 3 years ago

6b766f92

feat(analysis/convex/quasiconvex): A quasilinear function is either monotone or antitone (#17801)

YaelDillies committed 3 years ago

dad7ecf9

chore(algebra/group/conj): move out results about finiteness (#17789)

Ruben-VandeVelde committed 3 years ago

d4ebdc81

fix(scripts/port_comments): deal with files that have no header to insert below (#17797)

eric-wieser committed 3 years ago

32e4a38c

chore(nat/order/basic): remove implicit variables (#17707)

Multramate committed 3 years ago

acf5258c

feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)

joelriou committed 3 years ago

31019c25