mathlib documentation

ring_theory.localization.away.adjoin_root

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