Mathlib Changelog
v4
Changelog
About
Github
Theorem
StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x
Modification history
2025-11-27 13:47
Mathlib/RingTheory/Etale/StandardEtale.lean
feat(RingTheory): `IsStandardEtale` (#32138)
Added
StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x
View on Github →