isFractional_of_le — Mathlib

English

If I is contained in the underlying submodule of a fractional ideal J, then I is fractional.

Русский

Если I содержится в подмодуле дробного идеала J, то I дробен.

LaTeX

$${I : Submodule R P} \le J.coeToSubmodule \Rightarrow IsFractional\ S\ I$$

Lean4

theorem isFractional_of_le {I : Submodule R P} {J : FractionalIdeal S P} (hIJ : I ≤ J) : IsFractional S I :=
  by
  obtain ⟨a, a_mem, ha⟩ := J.isFractional
  use a, a_mem
  intro b b_mem
  exact ha b (hIJ b_mem)

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