Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-21 11:17 b3a21123

View on Github →

chore(algebra/group/conj): move conj_injective and use existing proofs (#5798)

Estimated changes

Modified src/algebra/group/conj.lean

added theorem conj_injective

Modified src/group_theory/order_of_element.lean

deleted theorem conj_injective