instIsScalarTowerSubtypeMemSubringToSubringOfPrime

English

IsScalarTower A (ofPrime A P).toSubring K holds; the tower aligns with the algebra map.

Русский

IsScalarTower A (ofPrime A P).toSubring K выполняется; тензорная башня согласуется с отображением через алгебраическую структуру.

LaTeX

$$IsScalarTower A (ofPrime A P).toSubring K$$

Lean4

instance : IsScalarTower A (ofPrime A P).toSubring K :=
  .of_algebraMap_eq
    (fun _ ↦ rfl)
      -- see https://github.com/leanprover-community/mathlib4/issues/29041

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