mul_generator_self_inv — Mathlib

English

For a principal fractional ideal I with a generator, I multiplied by the inverse of its generator equals 1.

Русский

Для порожденного дробного идеала I произведение на обратное порождение даёт 1.

LaTeX

$$$$I \cdot \mathrm{generator}(I)^{-1} = 1.$$$$

Lean4

theorem mul_generator_self_inv {R₁ : Type*} [CommRing R₁] [Algebra R₁ K] [IsLocalization R₁⁰ K]
    (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)] (h : I ≠ 0) :
    I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 := by
  -- Rewrite only the `I` that appears alone.

  conv_lhs => congr; rw [eq_spanSingleton_of_principal I]
  rw [spanSingleton_mul_spanSingleton, mul_inv_cancel₀, spanSingleton_one]
  intro generator_I_eq_zero
  apply h
  rw [eq_spanSingleton_of_principal I, generator_I_eq_zero, spanSingleton_zero]

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