Commit 2025-02-18 10:05 209440b4

View on Github →

fix(RingTheory/Ideal): make two Ideals in Ideal.Quotient.factor implicit (#22022) make two Ideals in Ideal.Quotient.factor implicit

Estimated changes

Modified Mathlib/Algebra/CharP/MixedCharZero.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Defs.lean

modified theorem Ideal.Quotient.factor_comp_mk

modified theorem Ideal.Quotient.factor_mk

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean