invPair — Mathlib

English

If σ₁: R1 → R2 and σ₂: R2 → R1 form a RingHomInvPair, then σ₁ is surjective.

Русский

Если σ₁: R1 → R2 и σ₂: R2 → R1 образуют RingHomInvPair, то σ₁ сюръективен.

LaTeX

$$$\forall y \in R_2,\exists x \in R_1:\ σ_{1}(x) = y$$$

Lean4

instance (priority := 100) invPair {σ₁ : R₁ →+* R₂} {σ₂ : R₂ →+* R₁} [RingHomInvPair σ₁ σ₂] : RingHomSurjective σ₁ :=
  ⟨fun x => ⟨σ₂ x, RingHomInvPair.comp_apply_eq₂⟩⟩

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