leanprover-community/mathlib3

Pull Requests Commits

Update src/group_theory/subgroup/basic.lean

thefundamentaltheor3m committed 3 years ago

Verified 9c65e532

add center_of_comm_eq_top

thefundamentaltheor3m committed 3 years ago

364f086e

add center_eq_top_of_comm

thefundamentaltheor3m committed 3 years ago

fb0bb795

center_eq_top_of_comm

thefundamentaltheor3m committed 3 years ago

9c229ddf

chore(data/nat,int): move field-specific lemmas about cast (#14890)

Vierkantor committed 3 years ago

44d3fc00

feat(data/set): replace `set_coe.can_lift` by `subtype.can_lift` (#14792)

urkud committed 3 years ago

c3e3d1aa

feat(analysis/../log): log_nat_eq_sum_factorization (#14782)

ericrbg committed 3 years ago

4de20c56

feat(data/polynomial/erase_lead): Characterizations of polynomials of small support (#14500)

tb65536 committed 3 years ago

c2fcf9f1

feat(order/hom/basic): some lemmas about order homs and equivs (#14872)

Paul-Lez committed 3 years ago

ef24aced

feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837)

jsm28 committed 3 years ago

dd2e7add

feat(group_theory/finite_abelian): Structure of finite abelian groups (#14736)

pbazin committed 3 years ago

966bb245

feat(analysis/seminorm): add add_group_seminorm (#14336)

mariainesdff committed 3 years ago

cff439d8

feat(number_theory): define ramification index and inertia degree (#14332)

Vierkantor committed 3 years ago

585a1bf3

feat(data/sigma,data/ulift,logic/equiv): add missing lemmas (#14903)

urkud committed 3 years ago

cc4b8e55

chore(number_theory/lucas_lehmer): remove `has_to_pexpr` instances (#14905)

eric-wieser committed 3 years ago

cf231995

chore(ring_theory/polynomial/symmetric): golf proofs (#14866)

eric-wieser committed 3 years ago

416edbd3

fix(meta/expr): remove `has_reflect.has_to_pexpr` (#14901)

eric-wieser committed 3 years ago

c45e5d58

chore(analysis/special_functions/log/basic): golf a proof (#14898)

urkud committed 3 years ago

2a732ed5

feat(order/filter/basic): add some lemmas about `eventually_le` (#14891)

kex-y committed 3 years ago

23918a54

refactor(data/set/countable): make `set.countable` protected (#14886)

urkud committed 3 years ago

12e5f2e0

refactor(data/finite/card): split from `basic` (#14885)

urkud committed 3 years ago

d8fc588d

feat(topology/basic): `sum.elim` of locally finite set families is locally finite (#14826)

urkud committed 3 years ago

c2719adf

feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824)

YaelDillies committed 3 years ago

44bb35e5

chore(data/rat): rename `data.rat.basic` to `data.rat.defs` (#14895)

Vierkantor committed 3 years ago

38642efc

chore(algebra/{group_power,order}): split off field lemmas (#14849)

Vierkantor committed 3 years ago

f57c0cdc

feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541)

fpvandoorn committed 3 years ago

d939b0e6

feat(set_theory/surreal/basic): define map `surreal →+o game` (#14783)

vihdzp committed 3 years ago

ad497685

feat(combinatorics/simple_graph/connectivity): Connectivity is a graph property (#14865)

YaelDillies committed 3 years ago

61b837fb

fix(tactic/apply_fun.lean): instantiate mvars in apply_fun (#14882)

digama0 committed 3 years ago

f3cd150b

chore(linear_algebra/alternating): more lemmas about `curry_left` (#14844)

eric-wieser committed 3 years ago

3b6552e0

Older