one_tmul_ground_apply' — Mathlib

English

The composition of polynomial laws is associative: h ∘ (g ∘ f) = (h ∘ g) ∘ f.

Русский

Сложение полиномальных законов по композиции ассоциативно: h ∘ (g ∘ f) = (h ∘ g) ∘ f.

LaTeX

$$$h \\circ (g \\circ f) = (h \\circ g) \\circ f$.$$

Lean4

theorem one_tmul_ground_apply' {S : Type u} [CommSemiring S] [Algebra R S] (x : M) :
    1 ⊗ₜ (f.ground x) = (f.toFun' S) (1 ⊗ₜ x) := by
  rw [ground_apply]
  convert f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)
  · simp only [includeRight_lid]
  · rw [rTensor_tmul, toLinearMap_apply, map_one]

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