prodCongr — Mathlib

English

If l: S ≃ₐ[R] A and r: T ≃ₐ[R] B are algebra isomorphisms, then their product l × r gives an algebra isomorphism (S × T) ≃ₐ[R] (A × B).

Русский

Если l: S ≃ₐ[R] A и r: T ≃ₐ[R] B — это изоморфизмы алгебр, то их произведение l × r задаёт изоморфизм алгебр (S × T) ≃ₐ[R] (A × B).

LaTeX

$$$$ (l : S \\simeq_{a[R]} A) \\times (r : T \\simeq_{a[R]} B) : (S \\times T) \\simeq_{a[R]} (A \\times B). $$$$

Lean4

/-- Product of algebra isomorphisms. -/
def prodCongr (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) : (S × T) ≃ₐ[R] A × B :=
  .ofRingEquiv (f := RingEquiv.prodCongr l r) <| by simp

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