monoidalFunctor_μ — Mathlib

English

The μ-structure of the discrete monoidal functor encodes the multiplication map for F, precisely μ(m1,m2) corresponds to the discrete equality from F.map_mul.

Русский

μ-структура дискретного моноидального функторa кодирует отображение умножения через F.map_mul.

LaTeX

$$$ \\mu(\\text{monoidalFunctor } F) m_1 m_2 = \\mathrm{Discrete.eqToHom}(F.map\\_mul\\,\\_\\_).\\mathrm{symm} $$$

Lean4

@[to_additive Discrete.addMonoidalFunctor_μ]
theorem monoidalFunctor_μ (F : M →* N) (m₁ m₂ : Discrete M) :
    μ (monoidalFunctor F) m₁ m₂ = Discrete.eqToHom (F.map_mul _ _).symm :=
  rfl

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