instIsScalarTower' — Mathlib

English

There is a scalar-tower structure on the inclusion of R into v.adicCompletionIntegers K v and then into v.adicCompletion K v; i.e., the associative law for smul holds.

Русский

Существует структура касания скаляров на включении R в v.adicCompletionIntegers K v и далее в v.adicCompletion K v; т.е. выполняется ассоциативное свойство умножения скаляров.

LaTeX

$$IsScalarTower R (v.adicCompletionIntegers K v) (v.adicCompletion K v)$$

Lean4

instance instIsScalarTower' : IsScalarTower R (v.adicCompletionIntegers K) (v.adicCompletion K) where
  smul_assoc x y z := by simp only [Algebra.smul_def]; apply mul_assoc

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