leanprover-community/mathlib3

Pull Requests Commits

feat(algebraic_geometry): Open covers of the fibred product. (#11733)

erdOne committed 3 years ago

a0bb6ea9

feat(topology/metric_space/basic): add some lemmas about spheres (#11719)

dupuisf committed 3 years ago

6130e571

feat(algebra/pointwise): introduce `canonically_ordered_comm_semiring` on `set_semiring` ... (#11580)

adomani committed 3 years ago

ca17a181

feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987)

vihdzp committed 3 years ago

719b7b06

feat(analysis/seminorm): define the topology induced by a family of seminorms (#11604)

mcdoll committed 3 years ago

750f53c8

feat(set_theory/ordinal_arithmetic): `lt_add_of_limit` (#11748)

vihdzp committed 3 years ago

ccbb8487

feat(model_theory/basic): define quotient structures (#11747)

awainverse committed 3 years ago

c0be8dcb

feat(group_theory/order_of_element): pow_eq_pow_iff_modeq (#11737)

ericrbg committed 3 years ago

792d3e56

feat(group_theory/nilpotent): abelian iff nilpotency class ≤ 1 (#11718)

nomeata committed 3 years ago

76b2a0ec

feat(algebra/squarefree): norm_num extension for squarefree (#11666)

digama0 committed 3 years ago

ff027743

feat(measure_theory): typeclass for measures positive on nonempty opens (#11652)

urkud committed 3 years ago

c04daaf4

feat(group_theory/nilpotent): add lemmas about `G / center G` (#11592)

nomeata committed 3 years ago

d6440a84

feat(topology/nhds_set): define neighborhoods of a set (#11520)

fpvandoorn committed 3 years ago

06bb5b66

feat(scripts/lint_style): Add a check for unfreeze_local_instances (#11509)

huynhtrankhanh committed 3 years ago

366d13ef

feat(order/hom/complete_lattice): Complete lattice homomorphisms (#11741)

YaelDillies committed 3 years ago

ada43f00

feat(category_theory/preadditive): the Yoneda embedding for preadditive categories (#11740)

TwoFX committed 3 years ago

08fed82d

feat(data/polynomial/reverse): lemmas about evaluating reversed polynomials (#11705)

Chris Hughes committed 3 years ago

323287e6

feat(data/{nat,int}/parity): add division lemmas (#11570)

user7230724 committed 3 years ago

bb2b58ed

feat(linear_algebra/{tensor,exterior,clifford}_algebra): these algebras are graded by powers of the submodules of their generators (#11542)

eric-wieser committed 3 years ago

6e016d21

refactor(order/bounded_order): Use `is_min`/`is_max` (#11408)

YaelDillies committed 3 years ago

45cfb254

feat(ring_theory/roots_of_unity): `fun_like` support (#11735)

ericrbg committed 3 years ago

2e1d8d67

feat(order/hom/lattice): Composition of lattice homs (#11676)

YaelDillies committed 3 years ago

406719e9

chore(analysis/inner_product_space/lax_milgram): docs fixes (#11745)

hrmacbeth committed 3 years ago

16274f60

feat(algebra/algebra/basic): add 1-related lemmas for `aut` (#11738)

ericrbg committed 3 years ago

43887435

feat(measure_theory/integral/lebesgue): weaken assumptions for with_density lemmas (#11711)

sgouezel committed 3 years ago

7468d8dd

feat(topology/algebra/continuous_monoid_hom): Add `topological_group` instance (#11707)

tb65536 committed 3 years ago

0c0ab69d

feat(data/set/lattice): review (#11672)

urkud committed 3 years ago

b3ad3f2a

feat(number_theory/cyclotomic): simplify `ne_zero`s (#11715)

ericrbg committed 3 years ago

6319a238

feat(ring_theory/roots_of_unity): turn `is_primitive_root` into a member of `roots_of_unity` (#11739)

ericrbg committed 3 years ago

8a67cf51

fix(tactic/suggest): make `library_search` aware of definition of `ne` (#11742)

arthurpaulino committed 3 years ago

50cdb957

Newer Older