Commit 2025-10-28 13:23 f1603113
View on Github →chore: deprecate duplicate Quotient{,Add}Group.kerLift_mk' (#30999) These were syntactically different in lean 3, but not in lean 4 due to the coercion expansion.
chore: deprecate duplicate Quotient{,Add}Group.kerLift_mk' (#30999) These were syntactically different in lean 3, but not in lean 4 due to the coercion expansion.