Theorem Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalars

Modification history

2025-11-27 13:47
Mathlib/RingTheory/Etale/Basic.lean
feat(RingTheory): `IsStandardEtale` (#32138)
Deleted Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalarsView on Github →
2025-11-17 16:19
Mathlib/RingTheory/Etale/Basic.lean
feat(RingTheory): miscellaneous lemmas about etale (#30857)
Added Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalarsView on Github →