IsFractional — Mathlib

English

A submodule I of a localized module is fractional if there exists a nonzero element a in S such that aI lies inside R.

Русский

Подмодуль I локализованного модуля является дробным, если существует ненулевой элемент a из S такой, что aI ⊆ R.

LaTeX

$$$IsFractional\\,S\\,I := \\exists a \\in S, \\forall b \\in I, IsInteger_R(a \\cdot b)$$$

Lean4

/-- A submodule `I` is a fractional ideal if `a I ⊆ R` for some `a ≠ 0`. -/
def IsFractional (I : Submodule R P) :=
  ∃ a ∈ S, ∀ b ∈ I, IsInteger R (a • b)

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