algebra' — Mathlib

English

There is a canonical algebra structure on S over R' induced from A via the inclusion S → A.

Русский

Существует каноническая структура алгебры на S над R', наследуемая от A через включение S ↪ A.

LaTeX

$$$\text{Algebra}(R', S)$$$

Lean4

instance (priority := 500) algebra' [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] : Algebra R' S
    where
  algebraMap :=
    (algebraMap R' A).codRestrict S fun x =>
      by
      rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ← Algebra.algebraMap_eq_smul_one]
      exact algebraMap_mem S _
  commutes' := fun _ _ => Subtype.eq <| Algebra.commutes _ _
  smul_def' := fun _ _ => Subtype.eq <| Algebra.smul_def _ _

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