isValuedIn_iff_mem_range — Mathlib

English

P.IsValuedIn S is equivalent to the root-pairings P.pairing i j belonging to the range of the algebra map from S to R for all i,j.

Русский

P.IsValuedIn S эквивалентно тому, что пары P.pairing i j принадлежат диапазону отображения алгебраMap S в R для всех i,j.

LaTeX

$$$$ P.IsValuedIn S \iff \forall i,j, \ P.pairing i j \in \mathrm{range}(\text{algebraMap } S R). $$$$

Lean4

theorem isValuedIn_iff_mem_range : P.IsValuedIn S ↔ ∀ i j, P.pairing i j ∈ range (algebraMap S R) := by
  simp only [isValuedIn_iff, mem_range]

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