coe_ext_iff — Mathlib

English

Two fractional ideals are equal iff their underlying submodules are equal after coe.

Русский

Два дробных идеала равны тогда и только тогда, когда их соответствующие подмодули после приведения к одному отображению совпадают.

LaTeX

$$$I = J \\;\\iff\\; (I : Submodule R P) = (J : Submodule R P)$$$

Lean4

/-- Partially-applied version of `FractionalIdeal.ext_iff`. -/
theorem coe_ext_iff {I J : FractionalIdeal S P} : I = J ↔ (I : Submodule R P) = (J : Submodule R P) :=
  Subtype.ext_iff

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