Commit 2024-07-27 08:25 6534c859

View on Github →

chore: robustifying for debug.byAsSorry (part 11) (#15169)

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Kernels.lean

Modified Mathlib/Algebra/Exact.lean

modified theorem Function.Exact.iff_of_ladder_addEquiv

modified theorem Function.Exact.of_ladder_addEquiv_of_exact'

modified theorem Function.Exact.of_ladder_addEquiv_of_exact

Modified Mathlib/Algebra/Homology/ShortComplex/Exact.lean

modified theorem CategoryTheory.ShortComplex.Exact.desc'

modified theorem CategoryTheory.ShortComplex.Exact.g_desc

modified theorem CategoryTheory.ShortComplex.Exact.isIso_f'

modified theorem CategoryTheory.ShortComplex.Exact.isIso_fromOpcycles

modified theorem CategoryTheory.ShortComplex.Exact.isIso_g'

modified theorem CategoryTheory.ShortComplex.Exact.isIso_toCycles

modified theorem CategoryTheory.ShortComplex.Exact.lift'

modified theorem CategoryTheory.ShortComplex.Exact.lift_f

modified theorem CategoryTheory.ShortComplex.Exact.map_of_epi_of_preservesCokernel

modified theorem CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel

Modified Mathlib/Algebra/Polynomial/Inductions.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

modified theorem Function.Injective.monic_map_iff

modified theorem Polynomial.degree_map_eq_of_injective

modified theorem Polynomial.leadingCoeff_map'

modified theorem Polynomial.leadingCoeff_of_injective

modified theorem Polynomial.monic_of_injective

modified theorem Polynomial.natDegree_map_eq_of_injective

modified theorem Polynomial.nextCoeff_map

Modified Mathlib/Algebra/Star/RingQuot.lean

modified theorem RingQuot.Rel.star

Modified Mathlib/Data/Finsupp/WellFounded.lean

modified theorem Finsupp.Lex.acc

modified theorem Finsupp.Lex.wellFounded'

modified theorem Finsupp.Lex.wellFounded

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified theorem Commute.isOfFinOrder_mul

modified theorem Commute.orderOf_dvd_lcm_mul

modified theorem Commute.orderOf_mul_dvd_lcm

modified theorem Commute.orderOf_mul_dvd_mul_orderOf

modified theorem Commute.orderOf_mul_eq_mul_orderOf_of_coprime

modified theorem Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.comap_isMaximal_of_surjective

modified theorem Ideal.comap_le_comap_iff_of_surjective

modified theorem Ideal.comap_map_of_surjective

modified theorem Ideal.map_eq_top_or_isMaximal_of_surjective

modified def Ideal.orderEmbeddingOfSurjective

modified def Ideal.relIsoOfSurjective

Modified Mathlib/RingTheory/Localization/FractionRing.lean