Commits leanprover-community/mathlib3

doc(data/countable/small): fix module docs (#15924)

urkud committed 3 years ago

dff563ec

feat(data/sign): more lemmas (#15917)

jsm28 committed 3 years ago

46ba96e7

feat(data/sym/sym2): `sym2.lift₂` (#15887)

vihdzp committed 3 years ago

a0c5aef8

feat(data/list/of_fn): last_of_fn (#15474)

pechersky committed 3 years ago

e992b757

feat(field_theory/polynomial_galois_group): add `mul_semiring_action` instance for `polynomial.gal` (#15914)

astrainfinita committed 3 years ago

9a4dde32

chore(data/multiset/basic): move theorems around (#15882)

vihdzp committed 3 years ago

1e594c77

feat(order/initial_seg): exchange `down` and `down'` (#15802)

vihdzp committed 3 years ago

0e9c7c16

chore(ring_theory/dedekind_domain): better, computable, defeq in `cancel_comm_monoid_with_zero` instance (#15752)

Vierkantor committed 3 years ago

530b948f

chore(order/well_founded): golf + rename variables (#15730)

vihdzp committed 3 years ago

05307825

feat(set_theory/zfc/basic): `pSet` with empty type is equivalent to `Ø` (#15550)

vihdzp committed 3 years ago

16478385

chore(analysis/convex/cone): fix typeclass assumption and add a missing lemma (#15879)

apurvnakade committed 3 years ago

9e9c3ab5

refactor(analysis/normed_space/operator_norm): generalize `continuous_linear_map.lmul` to non-unital algebras (#15868)

j-loreaux committed 3 years ago

a6b56ec2

feat(measure_theory/function/ae_eq_of_integral): remove a finite_measure assumption (#15899)

sgouezel committed 3 years ago

a97d85de

feat(analysis/normed_space/multilinear): constant scalar multiplication is continuous (#15897)

mcdoll committed 3 years ago

2be2f2cb

doc(linear_algebra/clifford_algebra/basic): docstring clarification (#15892)

kbuzzard committed 3 years ago

9a5b9842

feat(probability/upcrossing): Doob's upcrossing estimate (#14933)

kex-y committed 3 years ago

e2333f32

feat(topology/metric_space/*): `additive`/`multiplicative`/`order_dual` instances (#15704)

YaelDillies committed 3 years ago

14d34b71

feat(data/nat): Add new binary recursors; prove the relationship between `nat.bits` and other pieces of code (#14990)

prakol16 committed 3 years ago

e3d2f74c

feat(order/complete_lattice): add `equiv.supr_congr` and `equiv.supr_comp` lemmas (#15852)

j-loreaux committed 3 years ago

dffc243a

feat(algebra/order/ring): lt_mul_{left,right,self} (#15848)

pechersky committed 3 years ago

d5344df1

feat(topology/algebra/module/basic): continuous versions of `linear_map.comp_sub` and variants (#15870)

ADedecker committed 3 years ago

d1795d68

feat(algebraic_geometry/open_immersion): Restricting a morphism twice is isomorphic to one restriction. (#15710)

erdOne committed 3 years ago

68cc6138

feat(set_theory/game/nim): lemmas about `nim 1` (#14787)

vihdzp committed 3 years ago

2ddf74ab

feat(set_theory/game/nim): Grundy value in terms of right moves (#15410)

vihdzp committed 3 years ago

666c6e00

fix(probability/notation): add missing spaces around operators in notation (#15862)

eric-wieser committed 3 years ago

162413fa

chore(data/seq/*): trivial spacing fixes (#15847)

vihdzp committed 3 years ago

6120aac4

feat(data/real/ennreal): add instance linear_ordered_comm_monoid_with_zero ℝ≥0∞ (#15851)

j-loreaux committed 3 years ago

11cace15

chore(analysis/mean_inequalities_pow): weaken assumptions on rpow_add_le_rpow (#15823)

ericrbg committed 3 years ago

7eaf3412

feat(field_theory/splitting_field): If an intermediate field contains all of the roots, then the polynomial splits (#15658)

tb65536 committed 3 years ago

20f68fc8

feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index (#15316)

Vierkantor committed 3 years ago

4d59d4af