Commit 2024-07-26 01:01 8b4366d5

View on Github →

chore: robustifying for debug.byAsSorry (part 4) (#15125)

Estimated changes

Modified Mathlib/Algebra/CharZero/Lemmas.lean

Modified Mathlib/Algebra/Field/Rat.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

modified theorem Subgroup.Normal.conj_mem'

modified theorem Subgroup.Normal.mem_comm

modified theorem Subgroup.Normal.mem_comm_iff

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

modified def LinearMap.comp

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/Regular/SMul.lean

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

modified theorem CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Data/Finset/PiInduction.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/GroupTheory/Congruence/Basic.lean

Modified Mathlib/GroupTheory/Perm/List.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

modified def OreLocalization.universalMulHom