Commit 2025-07-08 17:55 7d2270ef

View on Github →

chore: fix a few typos in lemma names (#26904) Inspired by #mathlib4 > Let's catch typos! @ 💬.

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Map.lean

deleted theorem Submodule.map_iSup_comap_of_sujective

added theorem Submodule.map_iSup_comap_of_surjective

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

deleted theorem Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative

added theorem Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative

Modified Mathlib/LinearAlgebra/Lagrange.lean

added theorem Lagrange.nodalWeight_eq_eval_derivative_nodal

deleted theorem Lagrange.nodalWeight_eq_eval_nodal_derative

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

added theorem NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk

deleted theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk

Modified Mathlib/NumberTheory/PrimeCounting.lean

added theorem Nat.tendsto_primeCounting

deleted theorem Nat.tensto_primeCounting

Modified Mathlib/NumberTheory/SmoothNumbers.lean

deleted theorem Nat.smmoothNumbers_eq_factoredNumbers_primesBelow

added theorem Nat.smoothNumbers_eq_factoredNumbers_primesBelow

Modified Mathlib/RingTheory/Ideal/Pointwise.lean

deleted theorem Ideal.pointwise_smul_toAddSubGroup

added theorem Ideal.pointwise_smul_toAddSubgroup