leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

404f9851

chore(data/polynomial/ring_division): remove nontrivial assumptions

eric-wieser committed 3 years ago

c7e910fb

feat(linear_algebra/matrix): any matrix power can be expressed as sums of powers `0 ≤ k < fintype.card n`

eric-wieser committed 3 years ago

ebf8e67d

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

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

leanprover-community-bot committed 3 years ago

17b621c0

feat(topology/continuous_function/cocompact_maps): add the type of cocompact continuous maps (#12938)

j-loreaux committed 3 years ago

b6d246a6

feat(topology/metric_space/metrizable): define and use a metrizable typeclass (#12934)

sgouezel committed 3 years ago

221796ab

chore(nnreal): rename lemmas based on real.to_nnreal when they mention of_real (#12937)

sgouezel committed 3 years ago

5925650f

feat(topology/category/Born): The category of bornologies (#12045)

YaelDillies committed 3 years ago

21435715

Older