eq_restrictScalarsRange_iff — Mathlib

English

For every m ∈ M' and p ∈ P', p equals restrictScalarsRange i k hk f hf m if and only if k p equals f(i m).

Русский

Для каждого m ∈ M' и p ∈ P' верно, что p = restrictScalarsRange i k hk f hf m тогда и только тогда, когда k p = f(i m).

LaTeX

$$$p = restrictScalarsRange i k hk f hf m\quad\Longleftrightarrow\quad k p = f(i m).$$$

Lean4

@[simp]
theorem eq_restrictScalarsRange_iff (m : M') (p : P') : p = restrictScalarsRange i k hk f hf m ↔ k p = f (i m) := by
  rw [← restrictScalarsRange_apply i k hk f hf m, hk.eq_iff]

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