compAddChar_apply — Mathlib

English

The underlying function of the composition equals the composition of the underlying functions: coe(ψ ∘ f) = (coe ψ) ∘ (coe f).

Русский

Функционал композиции равен композиции функционалов: coe(ψ ∘ f) = (coe ψ) ∘ (coe f).

LaTeX

$$$$ \operatorname{coe}(\psi \circ f) = (\operatorname{coe}\psi) \circ (\operatorname{coe} f). $$$$

Lean4

@[simp, norm_cast]
theorem _root_.MonoidHom.compAddChar_apply (f : M →* N) (φ : AddChar A M) : f.compAddChar φ = f ∘ φ :=
  rfl

Похожие утверждения