leanprover-community/mathlib

Pull Requests Commits

add `mul_mem_coe` to help with elaboration

j-loreaux committed 3 years ago

Verified 2c273240

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

leanprover-community-bot committed 3 years ago

2b902eb3

feat(data/mv_polynomial/equiv): API for `mv_polynomial.fin_succ_equiv` (#10812)

isadofschi committed 3 years ago

79bc6ad4

feat(polynomial/cyclotomic): `eval_apply` (#13586)

ericrbg committed 3 years ago

17d24243

feat(data/quot): `quotient.out` is injective (#13584)

vihdzp committed 3 years ago

40fc58cb

doc(category_theory/limits/has_limits): fix two docstrings (#13581)

jcommelin committed 3 years ago

821e7c89

chore(set_theory/cardinal/basic): Fix spacing (#13562)

vihdzp committed 3 years ago

7b92db75

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

Older