restrictScalarsRange₂_apply — Mathlib

English

For all m ∈ M', n ∈ N', p ∈ P', p = restrictScalarsRange₂ i j k hk B hB m n if and only if k p = B(i m)(j n).

Русский

Для всех m ∈ M', n ∈ N', p ∈ P' верно, что p = restrictScalarsRange₂ i j k hk B hB m n тогда и только тогда, когда k p = B(i m)(j n).

LaTeX

$$$p = restrictScalarsRange_2(i,j,k hk B hB)(m,n)\iff k p = B(i m)(j n).$$$

Lean4

@[simp]
theorem restrictScalarsRange₂_apply (m : M') (n : N') : k (restrictScalarsRange₂ i j k hk B hB m n) = B (i m) (j n) :=
  by simp [restrictScalarsRange₂]

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