Theorems · Theorem · group theory

MulEquiv.mk.congr_simp

∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (toEquiv toEquiv_1 : M ≃ N)
  (e_toEquiv : toEquiv = toEquiv_1) (map_mul' : ∀ (x y : M), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y),
  { toEquiv := toEquiv, map_mul' := map_mul' } = { toEquiv := toEquiv_1, map_mul' := ⋯ }

Defined in

Mathlib.Algebra.Group.End

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

MulMul