mathlib3 documentation

ring_theory.localization.away.adjoin_root

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The R-alg_equiv between the localization of R away from r and R with an inverse of r adjoined.

The R-alg_equiv between the localization of R away from r and R with an inverse of r adjoined.

Equations