Commit 2025-10-06 14:25 f3ad651e

View on Github →

chore: golf entire epi_of_cokernel_π_eq_zero, bottom_row_coprime, congr_of_eventuallyEq and Invertible.congr (#28490)

Estimated changes

Modified Mathlib/Algebra/Group/Invertible/Defs.lean

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

modified theorem CategoryTheory.Abelian.epi_of_cokernel_π_eq_zero

Modified Mathlib/Topology/ContinuousOn.lean