Commit 2025-11-24 14:10 1764613b

View on Github →

feat(Algebra): characterise when a quotient is nontrivial (#31198) From BrauerGroup and ClassFieldTheory

Estimated changes

modified theorem Submodule.mem_top
modified theorem Submodule.top_toAddSubgroup
added theorem Setoid.mk_eq_bot
added theorem Setoid.mk_eq_top
added theorem Con.toSetoid_bot
added theorem Con.toSetoid_eq_bot
added theorem Con.toSetoid_eq_top
modified theorem Con.toSetoid_inj
added theorem Con.toSetoid_injective
added theorem Con.toSetoid_top
modified theorem RingCon.coe_bot
modified theorem RingCon.coe_top
modified theorem RingCon.le_def
added theorem RingCon.toCon_bot
added theorem RingCon.toCon_eq_bot
added theorem RingCon.toCon_eq_top
added theorem RingCon.toCon_top
added theorem RingCon.toCon_inj