Def Ideal.Quotient.algebraQuotientOfLEComap

Modification history

2024-12-10 15:20

Mathlib/RingTheory/Ideal/Over.lean

refactor/fix: don't use RingHom.toAlgebra in Ideal.quotientAlgebra (#19847)

Deleted Ideal.Quotient.algebraQuotientOfLEComap View on Github →

2023-09-08 15:47

Mathlib/RingTheory/Ideal/Over.lean

chore: tidy various files (#7035)

Added Ideal.Quotient.algebraQuotientOfLEComap View on Github →