smulTower_apply — Mathlib

English

The representation of smulTower is given by the composition of representations with reindexing.

Русский

Представление smulTower задаётся композицией представлений с перебазированием индексов.

LaTeX

$$$$ smulTower_repr : (b.repr) \circ (c.repr) \Rightarrow (smulTower) $$$$

Lean4

@[simp]
theorem smulTower_apply (ij) : (b.smulTower c) ij = b ij.1 • c ij.2 := by
  classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_apply, Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]

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