Commit 2024-07-26 09:13 918df05c

View on Github →

chore: robustifying for debug.byAsSorry (part 9) (#15150) See zulip.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

modified def LinearEquiv.extendScalarsOfSurjective

modified def LinearMap.extendScalarsOfSurjectiveEquiv

Modified Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

modified theorem Subalgebra.coe_iSup_of_directed

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified def MonoidAlgebra.equivariantOfLinearOfComm

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/CategoryTheory/GradedObject/Unitor.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

modified def CategoryTheory.Sheaf.Subcanonical.yoneda

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

modified theorem CategoryTheory.Functor.isContinuous_of_preservesOneHypercovers

Modified Mathlib/CategoryTheory/Sites/CoversTop.lean

modified theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.exists_unique_section

modified theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_apply

modified theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible

Modified Mathlib/CategoryTheory/Sites/Localization.lean

modified theorem CategoryTheory.GrothendieckTopology.W_adj_unit_app

modified theorem CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction

modified theorem CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

modified theorem SimpleGraph.IsTuranMaximal.degree_eq_of_not_adj

modified theorem SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph

modified theorem SimpleGraph.IsTuranMaximal.not_adj_trans

Modified Mathlib/Data/Finite/Card.lean

modified theorem Set.Finite.card_lt_card

Modified Mathlib/GroupTheory/QuotientGroup.lean

Modified Mathlib/Order/Filter/FilterProduct.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.comap_bot_le_of_injective

modified theorem Ideal.comap_bot_of_injective

modified theorem Ideal.comap_le_iff_le_map

modified theorem Ideal.map.isMaximal

modified def Ideal.relIsoOfBijective

Modified Mathlib/SetTheory/Cardinal/ToNat.lean

modified theorem Cardinal.toNat_apply_of_lt_aleph0

Modified Mathlib/SetTheory/Ordinal/Basic.lean