map — Mathlib

English

If A and B are linearly disjoint and f: S → T is an injective algebra homomorphism, then the images A.map f and B.map f are linearly disjoint in T.

Русский

Если A и B линейно дизъюнктны и f: S → T инъективно, то их образы A.map f и B.map f линейно дизъюнктны в T.

LaTeX

$$(A.map f).LinearDisjoint (B.map f)$$

Lean4

/-- Linear disjointness is preserved by injective algebra homomorphisms. -/
theorem map (H : A.LinearDisjoint B) {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ[R] T)
    (hf : Function.Injective f) : (A.map f).LinearDisjoint (B.map f) :=
  Submodule.LinearDisjoint.map H f hf

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