Commit 2023-02-15 04:55 5c795927

View on Github →

feat: port GroupTheory.Commensurable (#2293)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Commensurable.lean

added theorem Commensurable.comm

added theorem Commensurable.commensurable_conj

added theorem Commensurable.commensurable_inv

added def Commensurable.commensurator'

added theorem Commensurable.commensurator'_mem_iff

added def Commensurable.commensurator

added theorem Commensurable.commensurator_mem_iff

added theorem Commensurable.eq

added theorem Commensurable.equivalence

added def Commensurable.quotConjEquiv

added theorem Commensurable.symm

added theorem Commensurable.trans

added def Commensurable