toNonUnitalSubring' — Mathlib

English

The forgetful map from NonUnitalSubalgebra to NonUnitalSubring is an order-embedding.

Русский

Отображение от NonUnitalSubalgebra к NonUnitalSubring является вложением по порядку.

LaTeX

$$def toNonUnitalSubring' : NonUnitalSubalgebra(R,A) ↪o NonUnitalSubring A$$

Lean4

/-- The forgetful map from `NonUnitalSubalgebra` to `NonUnitalSubsemiring` as an
`OrderEmbedding` -/
def toNonUnitalSubring' [CommRing R] [NonUnitalNonAssocRing A] [Module R A] :
    NonUnitalSubalgebra R A ↪o NonUnitalSubring A
    where
  toEmbedding :=
    { toFun := fun S => S.toNonUnitalSubring
      inj' := fun S T h => ext <| by apply SetLike.ext_iff.1 h }
  map_rel_iff' := SetLike.coe_subset_coe.symm.trans SetLike.coe_subset_coe

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