Commit 2024-10-29 12:35 dfbe4365

View on Github →

chore(GroupTheory/Coset): split off Defs file (#18347) The goal of this PR is to have a file with the definitions for the quotient of a group, in terms of cosets. We include enough theory to put a group structure on the quotient by a normal group.

Estimated changes

deleted theorem QuotientGroup.exists_mk
deleted theorem QuotientGroup.forall_mk
deleted theorem QuotientGroup.leftRel_eq
deleted theorem QuotientGroup.out_eq'
deleted theorem QuotientGroup.range_mk
deleted theorem QuotientGroup.rightRel_eq
added theorem QuotientGroup.out_eq'
added theorem QuotientGroup.range_mk