leanprover-community/mathlib

Pull Requests Commits

feat(algebra/char_p): use `finite` instead of `fintype` (#16002)

urkud committed 3 years ago

2fae5fd7

feat(topology/separation): add `t0_space.of_cover` (#15982)

urkud committed 3 years ago

32a432cc

feat(ring_theory/algebraic): `alg_hom` from an algebraic extension to itself is bijective (#15873)

alreadydone committed 3 years ago

41cf8de0

feat(ring_theory/derivation): The kernel of the map `S ⊗[R] S →ₐ[R] S`. (#15856)

erdOne committed 3 years ago

d8531745

feat (data/multiset/powerset): add bind_powerset_len (#15824)

xroblot committed 3 years ago

87e9e26a

refactor(category_theory/lifting_properties): refactor lifting properties using comm_sq (#15765)

eric-wieser committed 3 years ago

796f2675

feat(combinatorics/set_family/compression/down): Down-compression (#15246)

YaelDillies committed 3 years ago

70d5733d

chore(order/conditionally_complete_lattice): `with_top.coe_infi` and `with_top.coe_supr` (#15975)

eric-wieser committed 3 years ago

8086825f

chore(data/mv_polynomial/basic): spacing (#16001)

vihdzp committed 3 years ago

a21a8bc6

feat(analysis/special_functions/trigonometric/angle): signs of angles (#15967)

jsm28 committed 3 years ago

50f092eb

doc(tactic/doc_commands): fix doc comment (#15947)

digama0 committed 3 years ago

bc40b44c

feat(archive/100-theorems-list): Königsberg bridges problem (#15279)

kmill committed 3 years ago

af8760cc

feat(algebra/group_with_zero/power): generalize `zpow_eq_zero_iff` (#15997)

urkud committed 3 years ago

bae872c3

refactor(set_theory/ordinal/cantor_normal_form): simplify `CNF` definition (#15449)

vihdzp committed 3 years ago

60a1dcf7

feat(category_theory/epi_mono): preserves/reflects properties for epi/split_epi (#15857)

joelriou committed 3 years ago

7af08859

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

leanprover-community-bot committed 3 years ago

dd6b84e2

feat(analysis/special_functions/trigonometric/chebyshev): `T_real_cos` and `U_real_cos` (#15798)

vihdzp committed 3 years ago

67821d26

feat(ring_theory/ideal): The module `I ⧸ I ^ 2`. (#15638)

erdOne committed 3 years ago

619eaf82

docs(topology/*/weak_dual): Add docstring (#15944)

mcdoll committed 3 years ago

299b6127

chore(category_theory/limits/*): Unify names for limit constructions. (#15810)

erdOne committed 3 years ago

3424a593

feat(data/fintype/basic): infinite.exists_superset_card_eq (#15787)

pechersky committed 3 years ago

43894fff

feat(field_theory/finite/basic): zmod.pow_totient is true for zero (#15771)

Ruben-VandeVelde committed 3 years ago

03d906cb

feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672)

jjaassoonn committed 3 years ago

286d6750

chore(topology/basic): update module docstring (#15976)

PatrickMassot committed 3 years ago

45ccb85d

chore(topology/algebra/uniform_mul_action): the action of a ring on itself is uniformly continuous (#15974)

eric-wieser committed 3 years ago

ac0996dd

feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966)

jsm28 committed 3 years ago

ce9af07f

feat(field_theory/intermediate_field): `minpoly K x = minpoly K (x : L)` (#15946)

tb65536 committed 3 years ago

452984bb

feat(category_theory/sites/subsheaf): Subpresheaves of types. (#15827)

erdOne committed 3 years ago

1e097351

feat(data/polynomial/{ basic + div + monic + degree/definitions }): lemmas about monic and forall_eq (#15817)

adomani committed 3 years ago

473da0e0

feat(measure_theory/measure/measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812)

ocfnash committed 3 years ago

7e33e4f1

Newer Older