Commit 2023-11-27 09:11 55eb8124

View on Github →

chore(GroupTheory/Congruence): small cleanups (#8314) Switches to where notation in a couple of places and removes a default lt field. Also replaces uses of .r with coeFn, since the latter is declared simp-normal by this file.

Estimated changes

added theorem Con.coe_inf
added theorem Con.coe_inj
added theorem Con.coe_sInf
modified theorem Con.conGen_le
modified theorem Con.ext'
deleted theorem Con.ext'_iff
deleted theorem Con.inf_def
deleted theorem Con.sInf_def
modified theorem Con.sup_def