Algebra generated by an integral unit #
This file records that over an Artinian commutative ring, the inverse of an integral unit belongs
to the algebra generated by that unit. The proof uses Mathlib's
IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor in the generated subalgebra.
Main declarations #
TauCeti.Units.coe_inv_mem_adjoin: the inverse of an integral unit is contained in the algebra generated by that unit.
theorem
TauCeti.Units.coe_inv_mem_adjoin
{K : Type u}
{A : Type v}
[CommRing K]
[IsArtinianRing K]
[Ring A]
[Algebra K A]
(u : Aˣ)
(hu : IsIntegral K ↑u)
:
The inverse of an integral unit over an Artinian commutative ring belongs to the algebra generated by that unit.