isScalarTower_mid' — Mathlib

English

Specialize the previous tower in the common case where the top field is L; i.e., IsScalarTower K S L.

Русский

Уточнение предыдущей башни в обычном случае, когда верхнее поле совпадает с L: IsScalarTower K S L.

LaTeX

$$$\\text{IsScalarTower } K\\, S\\, L$$$

Lean4

/-- Specialize `isScalarTower_mid` to the common case where the top field is `L`. -/
instance isScalarTower_mid' : IsScalarTower K S L :=
  inferInstance

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