Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 18:50 e789ad31

View on Github →

feat(group_theory/subgroup): mk lemmas (#9514) See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/set_like.20idiom

Estimated changes

added theorem submodule.coe_set_mk
added theorem submodule.mem_mk
deleted theorem submodule.mk_coe
added theorem submodule.mk_le_mk
added theorem subfield.coe_set_mk
modified theorem subfield.mem_mk
added theorem subfield.mk_le_mk
added theorem subgroup.coe_set_mk
added theorem subgroup.mem_mk
added theorem subgroup.mk_le_mk
added theorem submonoid.coe_set_mk
added theorem submonoid.mem_mk
added theorem submonoid.mk_le_mk
added theorem subring.coe_set_mk
added theorem subring.mem_mk
added theorem subring.mk_le_mk