isSMulRegular_algebraMap_iff — Mathlib

English

For an R–S algebra with suitable module structure, IsSmulRegular M (algebraMap r) is equivalent to IsSmulRegular M r.

Русский

Для алгеброкультурного отображения R→S и подходящей структуры модуля IsSmulRegular(M, algebraMap r) эквивалентна IsSmulRegular(M, r).

LaTeX

$$$IsSmulRegular\, M\; (\operatorname{algebraMap} \; r) \iff IsSmulRegular\, M\; r$.$$

Lean4

theorem isSMulRegular_algebraMap_iff [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M]
    [Module S M] [IsScalarTower R S M] (r : R) : IsSMulRegular M (algebraMap R S r) ↔ IsSMulRegular M r :=
  (Equiv.refl M).isSMulRegular_congr (algebraMap_smul S r)

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