English
Let I be a fractional ideal for which the underlying submodule is principal. Then I is invertible (i.e., I · I^{-1} = 1) if and only if the generator of I (as a principal submodule) is nonzero.
Русский
Пусть I — дробный идеал, для которого соответствующее подмодуль является порожденным порождающим. Тогда I обратим, т. е. I · I^{-1} = 1, тогда и только тогда, когда порождающая I не равна нулю.
LaTeX
$$$I \\cdot I^{-1} = 1 \\iff \\mathrm{generator}(I) \\neq 0$$$
Lean4
theorem invertible_iff_generator_nonzero (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)] :
I * I⁻¹ = 1 ↔ generator (I : Submodule R₁ K) ≠ 0 :=
by
constructor
· intro hI hg
apply ne_zero_of_mul_eq_one _ _ hI
rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]
· intro hg
apply invertible_of_principal
rw [eq_spanSingleton_of_principal I]
intro hI
have := mem_spanSingleton_self R₁⁰ (generator (I : Submodule R₁ K))
rw [hI, mem_zero_iff] at this
contradiction
