Commit 2025-02-23 23:17 d0fcbc38

View on Github →

chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem AlgHom.ker_coe_equiv

deleted theorem Ideal.AlgHom.coe_ker

added theorem Ideal.AlgHom.ker_coe