Theorem IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk

Modification history

2025-08-18 12:21
Mathlib/RingTheory/IsAdjoinRoot.lean
feat(RingTheory/IsAdjoinRoot): add properties and constructors (#27373) …
Added IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mkView on Github →