coeToSubmodule_eq_bot — Mathlib

English

The equality of the underlying submodule to the bottom submodule is equivalent to the ideal being zero.

Русский

Равенство подмодуля нулю эквивалентно нулевому идеалу.

LaTeX

$${I : FractionalIdeal S P} : (I : Submodule R P) = ⊥ ↔ I = 0$$

Lean4

theorem coeToSubmodule_eq_bot {I : FractionalIdeal S P} : (I : Submodule R P) = ⊥ ↔ I = 0 :=
  ⟨fun h => coeToSubmodule_injective (by simp [h]), fun h => by simp [h]⟩

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