smulOfTower — Mathlib

English

If b and c are related, then t•b and t•c are related for any tower action of S on R: Rel(R,X,b,c) ⇒ Rel(R,X,t•b,t•c).

Русский

Если b и c связаны, то t•b и t•c связаны при любом действии башни S на R.

LaTeX

$$$\text{Rel}(R,X,b,c) \Rightarrow \text{Rel}(R,X,t \cdot b,t \cdot c)$$$

Lean4

theorem smulOfTower {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (t : S) (a b : lib R X)
    (h : Rel R X a b) : Rel R X (t • a) (t • b) :=
  by
  rw [← smul_one_smul R t a, ← smul_one_smul R t b]
  exact h.smul _

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