Simple intermediate fields generated by inverses

Adjoining an element to a field is unchanged when that element is replaced by its inverse.

Main results

• TauCeti.IntermediateField.adjoin_simple_inv: K⟮x⁻¹⟯ = K⟮x⟯.

@[simp]

theorem TauCeti.IntermediateField.adjoin_simple_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : L) : K⟮x⁻¹⟯ = K⟮x⟯

The simple intermediate field generated by the inverse of an element is the one generated by the element itself.