isFractional_of_le_one — Mathlib

English

If I ≤ J.coeToSubmodule for some fractional ideal J, then I is fractional.

Русский

Если I ≤ J.coeToSubmodule для некоторого дробного идеала J, то I является дробным.

LaTeX

$$$I \le J.\mathrm{coeToSubmodule} \Rightarrow IsFractional\ S\ I$$$

Lean4

theorem isFractional_of_le_one (I : Submodule R P) (h : I ≤ 1) : IsFractional S I :=
  by
  use 1, S.one_mem
  intro b hb
  rw [one_smul]
  obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)
  exact Set.mem_range_self b'

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