instIsScalarTower — Mathlib

English

IsScalarTower for Clifford algebras relating R, S, A structures in a multi-layer tower; ensures compatible scalar actions across layers.

Русский

IsScalarTower для клиффордовых алгебр, устанавливающий совместимые действия над скалярами на нескольких слояхTower.

LaTeX

$$$\text{IsScalarTower } R S (\mathrm{CliffordAlgebra}\ Q)$$$

Lean4

instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A] [SMul R S] [Algebra R A]
    [Algebra S A] [Module R M] [Module S M] [Module A M] [IsScalarTower R A M] [IsScalarTower S A M]
    [IsScalarTower R S A] (Q : QuadraticForm A M) : IsScalarTower R S (CliffordAlgebra Q) :=
  RingQuot.instIsScalarTower _

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