leanprover-community/mathlib

Pull Requests Commits

fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544)

eric-wieser committed 3 years ago

1da12b57

refactor(category_theory): make has_zero_object a Prop (#13517)

jcommelin committed 3 years ago

77236cd2

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13475)

tb65536 committed 3 years ago

dced1336

chore(*): remove `subst` when not necessary (#13453)

ericrbg committed 3 years ago

bb9d1c50

feat(linear_algebra/prod): two lemmas about prod_map (#13572)

antoinelab01 committed 3 years ago

afb43923

feat(group_theory/transfer): Define the transfer homomorphism (#13446)

tb65536 committed 3 years ago

d444a279

feat(ring_theory/valuation/valuation_subring): The order structure on valuation subrings of a field (#13429)

adamtopaz committed 3 years ago

b1a1ece3

feat(topology/constructions): more convenient lemmas (#13423)

fpvandoorn committed 3 years ago

1e76b9eb

feat(algebra/big_operators): split products and sums over fin (a+b) (#13291)

joelriou committed 3 years ago

63ee5582

feat(group_theory/torsion): torsion-free groups and quotients by torsion subgroups (#13173)

Julian committed 3 years ago

4d7683b2

feat(order/grade): Graded orders (#11308)

YaelDillies committed 3 years ago

e728cfd4

feat(number_theory/modular): fundamental domain part 2 (#8985)

AlexKontorovich committed 3 years ago

8110ab9d

chore(algebra/algebra/spectrum): lemmas about the zero ring (#13568)

eric-wieser committed 3 years ago

ba556a70

ci(gitpod): update leanproject version (#13567)

eric-wieser committed 3 years ago

81453334

chore(set_theory/ordinal/basic): Small style tweaks (#13561)

vihdzp committed 3 years ago

aeef727f

refactor(group_theory/{submonoid, subsemigroup}/basic): move `mul_mem_class` (#13559)

j-loreaux committed 3 years ago

efab188a

feat(data/nat/pow): add theorem `nat.pow_mod` (#13551)

slerpyyy committed 3 years ago

afe14217

feat(analysis/normed_space/operator_norm): norm of `lsmul` (#13538)

fpvandoorn committed 3 years ago

090e59d0

feat(algebra/group_power/lemmas): More lemmas through `to_additive` (#13537)

YaelDillies committed 3 years ago

8430aae3

feat(data/real/ennreal): `tsub` lemmas (#13525)

YaelDillies committed 3 years ago

08323cda

refactor(category_theory): reverse simp lemmas about (co)forks (#13519)

javra committed 3 years ago

3a061790

chore(set_theory/game/*): Protect ambiguous lemmas (#13557)

YaelDillies committed 3 years ago

b7cba576

feat(combinatorics/simple_graph/clique): Clique-free graphs (#13552)

YaelDillies committed 3 years ago

b6c96ef7

feat(analysis/calculus/cont_diff): add more prod lemmas (#13521)

fpvandoorn committed 3 years ago

e49ac91b

chore(algebra/star/chsh): `repeat`ed golf (#13499)

adomani committed 3 years ago

62b33339

feat(measure_theory/measure/measure_space): add some lemmas for the counting measure (#13485)

kex-y committed 3 years ago

777d1ec1

feat(topology/instances/ennreal): Add lemmas about continuity of ennreal subtraction. (#13448)

kkytola committed 3 years ago

6490ee3a

feat(algebra/monoid_algebra/basic): lifts of (add_)monoid_algebras (#13382)

adomani committed 3 years ago

91cbe460

feat(topology/algebra/module/basic): continuous linear maps are automatically uniformly continuous (#13276)

ADedecker committed 3 years ago

8044794f

fix(tactic/apply_rules): separate single rules and attribute names in syntax (#13227)

robertylewis committed 3 years ago

79abf670

Newer Older