Theorem AlgEquiv.coe_extendScalarsOfSurjective

Modification history

2026-04-13 10:18
Mathlib/Algebra/Algebra/Tower.lean
refactor(Algebra): replace `RingEquivClass.toRingEquiv` by structure-specific coercions (#21031) …
Added AlgEquiv.coe_extendScalarsOfSurjectiveView on Github →