Theorem conj_mul

Modification history

2026-03-25 15:49

Mathlib/Algebra/Group/Conj.lean

refactor(GroupTheory/Commutator/Basic): to_additivize commutators (#34784) …

Modified conj_mul View on Github →

2022-12-22 03:31

Mathlib/Algebra/Group/Conj.lean

feat: port algebra.group.conj (#1158) …

Added conj_mul View on Github →