Commit 2020-05-13 07:01 ed183f95
View on Github →chore(group_theory/submonoid): use complete_lattice_of_Inf
(#2661)
- Use
complete_lattice_of_Inf
forsubmonoid
andsubgroup
lattices. - Add
sub*.copy
. - Add a few
@[simp]
lemmas.
chore(group_theory/submonoid): use complete_lattice_of_Inf
(#2661)
complete_lattice_of_Inf
for submonoid
and subgroup
lattices.sub*.copy
.@[simp]
lemmas.