Theorems · Theorem · ring theory

Unitary.mapEquiv_apply

∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R ≃⋆* S) (a : ↥(unitary R)), (Unitary.mapEquiv f) a = (Unitary.map f.toStarMonoidHom) a

Defined in

Mathlib.Algebra.Star.Unitary

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

MonoidStarMulMonoidStarMul