Commit 2024-07-25 23:15 812755da

View on Github →

Chore: robustifying for debug.byAsSorry (part 7) (#15137) cf #15126 and #15133

Estimated changes

Modified Mathlib/Algebra/BigOperators/Associated.lean

modified theorem Prime.exists_mem_finset_dvd

modified theorem Prime.exists_mem_multiset_dvd

modified theorem Prime.exists_mem_multiset_map_dvd

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Modified Mathlib/Algebra/Order/Module/Defs.lean

modified theorem PosSMulMono.lift

modified theorem PosSMulReflectLE.lift

modified theorem PosSMulReflectLT.lift

modified theorem PosSMulStrictMono.lift

modified theorem SMulPosMono.lift

modified theorem SMulPosReflectLE.lift

modified theorem SMulPosReflectLT.lift

modified theorem SMulPosStrictMono.lift

Modified Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

modified theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_left

modified theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_right

modified theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_left

modified theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_right

modified theorem Commute.pow_dvd_pow_of_add_pow_eq_zero

modified theorem Commute.pow_dvd_pow_of_sub_pow_eq_zero

modified theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_left

modified theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_right

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Data/Fintype/Order.lean

modified theorem Directed.finite_le

modified theorem Directed.finite_set_le

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Order/BooleanGenerators.lean

modified theorem IsCompactlyGenerated.BooleanGenerators.atomistic

modified def IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top

modified theorem IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top

modified def IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top

modified theorem IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top

modified theorem IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top

modified theorem IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms

modified theorem IsCompactlyGenerated.BooleanGenerators.mono

modified theorem IsCompactlyGenerated.BooleanGenerators.sSup_inter

modified theorem IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms

Modified Mathlib/Order/Interval/Finset/Defs.lean

modified theorem Finset.map_subtype_embedding_Icc

modified theorem Finset.map_subtype_embedding_Ico

modified theorem Finset.map_subtype_embedding_Ioc

modified theorem Finset.map_subtype_embedding_Ioo

Modified Mathlib/RingTheory/Nilpotent/Basic.lean

modified theorem Commute.add_pow_add_eq_zero_of_pow_eq_zero

modified theorem Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero

modified theorem Commute.isNilpotent_add

modified theorem Commute.isNilpotent_sub