Commits leanprover-community/mathlib3

feat(data/nat/factorization): add lemma `factorization_le_iff_dvd` (#11377)

stuart-presnell committed 4 years ago

647598bd

fix(algebra/tropical/basic): provide explicit min and max (#11380)

eric-wieser committed 4 years ago

a5f79090

feat(algebra/indicator_function): add primed version for `mul_indicator_mul` and `indicator_sub` (#11379)

kex-y committed 4 years ago

73847ff3

feat(data/real/ennreal): add ennreal lemma for `a / 3 + a / 3 + a / 3 = a` (#11378)

kex-y committed 4 years ago

d1c49616

feat(group_theory/free_group): promote free_group_congr to a mul_equiv (#11373)

eric-wieser committed 4 years ago

57a8933b

feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372)

YaelDillies committed 4 years ago

8db96a8f

feat(ring_theory/witt_vector): Witt vectors over a domain are a domain (#11346)

robertylewis committed 4 years ago

93e77412

feat(analysis/complex/isometry): `rotation` matrix representation and determinant (#11339)

jsm28 committed 4 years ago

83b03557

feat(data/complex/module,data/complex/determinant): `conj_ae` matrix representation and determinant (#11337)

jsm28 committed 4 years ago

e4a41e6f

feat(algebra/*): injective hom into kernel `map_eq_*_iff` (#11275)

pechersky committed 4 years ago

aa7a439d

feat(order/minimal): Subset of minimal/maximal elements (#11268)

YaelDillies committed 4 years ago

94fd004d

feat(data/polynomial/degree/lemmas): add induction principle for non-constant polynomials (#8463)

adomani committed 4 years ago

490847ee

chore(*): update to 3.38.0c (#11371)

gebner committed 4 years ago

b7107717

refactor(ring_theory/discriminant): refactor discr_not_zero_of_linear_independent (#11370)

riccardobrasca committed 4 years ago

b8d2affd

chore(set_theory/ordinal_arithmetic): Golfed some proofs (#11369)

vihdzp committed 4 years ago

380e28e9

feat(analysis/asymptotics/asymptotics): add `is_bounded_under.is_O_const` (#11367)

urkud committed 4 years ago

2963d7ce

refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365)

urkud committed 4 years ago

8f5303ae

feat(analysis/calculus/{f,}deriv): add some `iff` lemmas (#11363)

urkud committed 4 years ago

c1c0fa4a

feat(algebra/group/conj): `conj_classes.map` preserves surjectivity (#11362)

tb65536 committed 4 years ago

02181c76

feat(topology): a few simple lemmas (#11360)

urkud committed 4 years ago

c94a17c7

chore(order/basic): Rename `no_bot_order`/`no_top_order` to `no_min_order`/`no_max_order` (#11357)

YaelDillies committed 4 years ago

56d6a915

feat(scripts/lint_mathlib): implement github annotations for mathlib linters (#11345)

alexjbest committed 4 years ago

be4c5aa4

feat(algebra/big_operators/finprod): `finprod_eq_one_of_forall_eq_one` (#11335)

pechersky committed 4 years ago

e138d3bb

feat(algebra/order/field): lemmas relating `a / b` and `a` when `1 ≤ b` and `1 < b` (#11333)

arthurpaulino committed 4 years ago

eb9c1525

refactor(data/set/prod): add notation class for set-like product (#11300)

urkud committed 4 years ago

2865d8c2

feat(ring_theory/polynomial/cyclotomic/basic): add lemmas (#11266)

riccardobrasca committed 4 years ago

3cd9088b

feat(data/dfinsupp/interval): Finitely supported dependent functions to locally finite orders are locally finite (#11175)

YaelDillies committed 4 years ago

4ac13d92

feat(category_theory): `Cat` is a strict bicategory (#11348)

yuma-mizuno committed 4 years ago

40b6b45c

feat(ring_theory/hahn_series): order_pow (#11334)

pechersky committed 4 years ago

a4052f90

feat(algebraic_geometry): Define the category of `AffineScheme`s (#11326)

erdOne committed 4 years ago

90ba0541