coeToSubmodule_ne_bot — Mathlib

English

Let I be a fractional ideal of S in P. Then the underlying R-submodule ↑I is nonzero if and only if I ≠ 0.

Русский

Пусть I -- дробный идеал над S в P. Тогда сопряжённое к нему R-подприведение ↑I не равно нулю тогда и только тогда, когда I ≠ 0.

LaTeX

$$$\uparrow I \neq \bot \iff I \neq 0$$$

Lean4

theorem coeToSubmodule_ne_bot {I : FractionalIdeal S P} : ↑I ≠ (⊥ : Submodule R P) ↔ I ≠ 0 :=
  not_iff_not.mpr coeToSubmodule_eq_bot

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