Commits leanprover-community/mathlib3

feat(analysis/normed_space): generalize some lemmas (#12959)

urkud committed 3 years ago

33afea82

feat(data/polynomial/erase_lead + data/polynomial/reverse): rename an old lemma, add a stronger one (#12909)

adomani committed 3 years ago

c65d8079

feat(analysis/inner_product_space): an inner product space is strictly convex (#12790)

urkud committed 3 years ago

7a1e0f20

chore(data/polynomial/degree/lemmas + data/polynomial/ring_division): move lemmas, reduce assumptions, golf (#12858)

adomani committed 3 years ago

1e72d86f

feat(analysis/von_neumann): concrete and abstract definitions of a von Neumann algebra (#12329)

kim-em committed 3 years ago

e5cd2ea1

feat(data/zmod/basic): add `int_coe_eq_int_coe_iff_dvd_sub` (#12944)

MichaelStollBayreuth committed 3 years ago

1494a9b2

feat(measure_theory/measure/measure_space): remove measurable_set assumption in ae_measurable.subtype_mk (#12978)

sgouezel committed 3 years ago

d620ad3c

merge

kim-em committed 3 years ago

a2c1d8bb

chore(model_theory/*): Split up big model theory files (#12918)

awainverse committed 3 years ago

2c6df07f

chore(scripts): update nolints.txt (#12971)

leanprover-community-bot committed 3 years ago

57a5fd72

chore(data/set/intervals/ord_connected): Golf proof (#12923)

vihdzp committed 3 years ago

664247fc

refactor(topology/instances/ennreal): make `ennreal` an instance of `has_continuous_inv` (#12806)

j-loreaux committed 3 years ago

05ef6940

refactor(category_theory/abelian): deduplicate definitions of (co)image (#12902)

kim-em committed 3 years ago

caf6f192

feat(ring_theory/polynomial/eisenstein): add cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at (#12707)

riccardobrasca committed 3 years ago

f5a9d0a3

refactor(data/list/basic): Remove many redundant hypotheses (#12950)

vihdzp committed 3 years ago

7b938899

feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947)

adomani committed 3 years ago

e63e3322

fix(data/set/prod): fix the way `×ˢ` associates (#12943)

fpvandoorn committed 3 years ago

b30f25ce

chore(data/equiv): split and move to `logic/equiv` (#12929)

Vierkantor committed 3 years ago

cc8c90d4

feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794)

YaelDillies committed 3 years ago

434a938b

chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952)

sgouezel committed 3 years ago

1f11f3f3

chore(measure_theory/integral/lebesgue): extend to ae_measurable (#12953)

sgouezel committed 3 years ago

a491055c

feat(measure_theory/constructions/borel_space): drop a countability assumption (#12954)

sgouezel committed 3 years ago

cb2797ee

chore(measure_theory/measure/lebesgue): delete leftovers (#12951)

sgouezel committed 3 years ago

b7d9166a

feat(topology/bases): separable subsets of topological spaces (#12936)

sgouezel committed 3 years ago

11114823

feat(topology/constructions): continuity of uncurried functions when the first factor is discrete (#12935)

sgouezel committed 3 years ago

f68536e0

feat(algebra/is_prime_pow): add `is_prime_pow_iff_factorization_single` (#12167)

stuart-presnell committed 3 years ago

5e449c20

feat(logic/nontrivial): `exists_pair_lt` (#12925)

vihdzp committed 3 years ago

023a7838

feat(set_theory/cardinal_ordinal): `κ ^ n = κ` for infinite cardinals (#12922)

vihdzp committed 3 years ago

c51f4f10

feat(topology/instances/ennreal): add `ennreal.has_sum_to_real` (#12926)

urkud committed 3 years ago

9d26041f

feat(linear_algebra/sesquilinear_form): add nondegenerate (#12683)

mcdoll committed 3 years ago

b83bd25d