Commits leanprover-community/mathlib3

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

feat(algebra/order/group/defs): add choice-free shortcut instances for `ordered_comm_group` (#17564)

astrainfinita committed 3 years ago

011aebd9

doc(tactic/congr): add relationship to `move_add` in `ac_change` (#14618)

adomani committed 3 years ago

28b66e1a

feat(topology/algebra/module/finite_dimension): `can_lift` instances (#17773)

YaelDillies committed 3 years ago

246853d5

feat(quiver/basic): push arrows of a quiver along a map (#17618)

bottine committed 3 years ago

7ba713a7

chore(algebra/star/basic): split out `big_operators` import (#17792)

hrmacbeth committed 3 years ago

6f6739f8

chore(data/set/pointwise/basic): split (#17768)

hrmacbeth committed 3 years ago

9114ddff

feat({data/finset/basic, ring_theory/roots_of_unity, algebra/ring/units}): add lemmas (#17671)

riccardobrasca committed 3 years ago

084ba5e0

chore(measure_theory/measurable_space_def): delete unused import (#17799)

hrmacbeth committed 3 years ago

94c141ac