Theorem Subalgebra.coe_equivMapOfInjective_apply

Modification history

2024-01-15 19:14
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
feat: add `equivMap[OfInjective]` for subalgebra and intermediate field (#9709) …
Added Subalgebra.coe_equivMapOfInjective_applyView on Github →