Commit 2026-10-13 21:09 b9c0df86

View on Github →

chore: fix misspellings in declaration names (#44823) This fixes misspellings in declaration names, such as fullyFaihtful, cocyle and diagaonal. 🤖 Generated with Claude Code

Estimated changes

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

Modified Mathlib/Algebra/Homology/ModelCategory/Lifting.lean

added theorem CochainComplex.Lifting.comp_coe_cocycle₁'_v_eq_zero

deleted theorem CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero

Modified Mathlib/CategoryTheory/Triangulated/TStructure/Induced.lean

added theorem CategoryTheory.ObjectProperty.mem_of_hasInducedTStructure

deleted theorem CategoryTheory.ObjectProperty.mem_of_hasInductedTStructure

Modified Mathlib/Data/Finset/Sups.lean

added theorem Finset.empty_diffs

deleted theorem Finset.empty_sdiffs

Modified Mathlib/GroupTheory/Focal.lean

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

deleted theorem RootPairing.Base.exists_cartanMatrix_diagaonal_mul_posDef

added theorem RootPairing.Base.exists_cartanMatrix_diagonal_mul_posDef

deleted theorem RootPairing.Base.exists_cartanMatrix_mul_diagaonal_posDef

added theorem RootPairing.Base.exists_cartanMatrix_mul_diagonal_posDef

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

deleted theorem PadicSeq.ne_zero_iff_nequiv_zero

added theorem PadicSeq.ne_zero_iff_not_equiv_zero

Modified Mathlib/Topology/Semicontinuity/Basic.lean

deleted theorem lowerSemicontinuouAt_inv_iff

added theorem lowerSemicontinuousAt_inv_iff