Commit 2024-01-15 19:14 6e66ddcd

View on Github →

feat: add equivMap[OfInjective] for subalgebra and intermediate field (#9709) ... parallel to Subring.equivMapOfInjective, Subsemiring.equivMapOfInjective, etc. etc.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

added theorem Subalgebra.coe_equivMapOfInjective_apply

added theorem Subalgebra.range_comp_val

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.coe_equivMap_apply

added theorem IntermediateField.fieldRange_comp_val

Modified Mathlib/FieldTheory/IntermediateField.lean