Commit 2024-08-01 00:14 0cafb4a8

View on Github →

chore: robustifying for debug.byAsSorry (part 14) (#15247)

Estimated changes

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

modified theorem QuasispectrumRestricts.algebraMap_image

modified theorem QuasispectrumRestricts.apply_mem

modified theorem QuasispectrumRestricts.image

modified theorem QuasispectrumRestricts.subset_preimage

modified theorem SpectrumRestricts.algebraMap_image

modified theorem SpectrumRestricts.apply_mem

modified theorem SpectrumRestricts.image

modified theorem SpectrumRestricts.subset_preimage

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

modified theorem Polynomial.aeval_apply_smul_mem_of_le_comap

Modified Mathlib/LinearAlgebra/Basis.lean

modified def Basis.mapCoeffs

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

modified theorem LinearMap.IsAlt.isRefl

modified theorem LinearMap.IsAlt.neg

modified theorem LinearMap.IsAlt.ortho_comm

Modified Mathlib/ModelTheory/Substructures.lean

modified def FirstOrder.Language.LHom.substructureReduct

modified def FirstOrder.Language.Substructure.gciMapComap