leanprover-community/mathlib3

Pull Requests Commits

returning to this

AlexKontorovich committed 3 years ago

2764c18b

last pre-clean version

AlexKontorovich committed 3 years ago

70aed0fc

AlexKontorovich committed 3 years ago

cdfe4d6d

feat(linear_algebra/span, matrix, finite_dimensional): new lemmas (#16006)

alreadydone committed 3 years ago

e2ba6de0

feat(topology/algebra/uniform_group): drop commutativity assumption in `topological_group.to_uniform_space` (#16004)

ocfnash committed 3 years ago

66b8fa75

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

Older