Theorems · Theorem · group theory

MulEquiv.symm_map_mul

∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (h : M ≃* N) (x y : N),
  h.symm (x * y) = h.symm x * h.symm y

An alias for h.symm.map_mul. Introduced to fix the issue in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth

Defined in

Mathlib.Algebra.Group.Equiv.Defs

Cited by

3 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

MulMul