lflip_apply — Mathlib

English

The map lflip sends f to f.flip; applying lflip to f gives the flipped map.

Русский

Пусть f — билинейное отображение; применение lflip возвращает f.flip.

LaTeX

$$$ lflip (f) = f.flip $$$

Lean4

@[simp]
theorem lflip_apply {R₀ : Type*} [Semiring R₀] [Module R₀ P] [SMulCommClass S₂ R₀ P] [SMulCommClass R₂ R₀ P]
    (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : lflip (R₀ := R₀) f = f.flip :=
  rfl

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