Commit 2026-10-26 16:38 79c6d249

View on Github →

chore: rename nonzero to ne_zero in theorem names (#44824) This renames theorems whose nonzero stands for a ≠ 0 hypothesis or conclusion to use ne_zero. 🤖 Generated with Claude Code

Estimated changes

Modified Mathlib/Algebra/Group/Fin/Tuple.lean

added theorem Matrix.cons_ne_zero_iff

deleted theorem Matrix.cons_nonzero_iff

Modified Mathlib/Algebra/Lie/Weights/IsSimple.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

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

Modified Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean

deleted theorem Polynomial.cardPowDegree_nonzero

added theorem Polynomial.cardPowDegree_of_ne_zero

Modified Mathlib/Algebra/Polynomial/Degree/Support.lean

added theorem Polynomial.natDegree_mem_support_of_ne_zero

deleted theorem Polynomial.natDegree_mem_support_of_nonzero

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

added theorem Polynomial.natTrailingDegree_mem_support_of_ne_zero

deleted theorem Polynomial.natTrailingDegree_mem_support_of_nonzero

added theorem Polynomial.trailingCoeff_ne_zero

deleted theorem Polynomial.trailingCoeff_nonzero_iff_nonzero

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Polynomial/EraseLead.lean

Modified Mathlib/Algebra/Polynomial/Reverse.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

deleted theorem Polynomial.aroots_smul_nonzero

added theorem Polynomial.aroots_smul_of_ne_zero

deleted theorem Polynomial.roots_smul_nonzero

added theorem Polynomial.roots_smul_of_ne_zero

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

added theorem AnalyticAt.exists_eventuallyEq_pow_smul_ne_zero_iff

deleted theorem AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff

added theorem AnalyticAt.unique_eventuallyEq_pow_smul_ne_zero

deleted theorem AnalyticAt.unique_eventuallyEq_pow_smul_nonzero

added theorem AnalyticAt.unique_eventuallyEq_zpow_smul_ne_zero

deleted theorem AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero

Modified Mathlib/Analysis/Analytic/Order.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added theorem constFormalMultilinearSeries_apply_of_ne_zero

deleted theorem constFormalMultilinearSeries_apply_of_nonzero

Modified Mathlib/Analysis/Complex/Periodic.lean

added theorem Function.Periodic.cuspFunction_eq_of_ne_zero

deleted theorem Function.Periodic.cuspFunction_eq_of_nonzero

Modified Mathlib/Analysis/InnerProductSpace/OfNorm.lean

Modified Mathlib/Analysis/LocallyConvex/Separation.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean

added theorem seminormFromBounded_ne_zero

deleted theorem seminormFromBounded_nonzero

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.I_mul_I_of_ne_zero

deleted theorem RCLike.I_mul_I_of_nonzero

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

added theorem CategoryTheory.Limits.cokernel_not_iso_of_ne_zero

deleted theorem CategoryTheory.Limits.cokernel_not_iso_of_nonzero

added theorem CategoryTheory.Limits.cokernel_not_mono_of_ne_zero

deleted theorem CategoryTheory.Limits.cokernel_not_mono_of_nonzero

added theorem CategoryTheory.Limits.kernel_not_epi_of_ne_zero

deleted theorem CategoryTheory.Limits.kernel_not_epi_of_nonzero

added theorem CategoryTheory.Limits.kernel_not_iso_of_ne_zero

deleted theorem CategoryTheory.Limits.kernel_not_iso_of_nonzero

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

added theorem CategoryTheory.Limits.image_ne_zero_of_ne_zero

deleted theorem CategoryTheory.Limits.nonzero_image_of_nonzero

Modified Mathlib/CategoryTheory/Preadditive/Schur.lean

added theorem CategoryTheory.isIso_iff_ne_zero

deleted theorem CategoryTheory.isIso_iff_nonzero

added theorem CategoryTheory.mono_of_ne_zero_from_simple

deleted theorem CategoryTheory.mono_of_nonzero_from_simple

Modified Mathlib/CategoryTheory/Simple.lean

added theorem CategoryTheory.cokernel_zero_of_ne_zero_to_simple

deleted theorem CategoryTheory.cokernel_zero_of_nonzero_to_simple

added theorem CategoryTheory.epi_of_ne_zero_to_simple

deleted theorem CategoryTheory.epi_of_nonzero_to_simple

added theorem CategoryTheory.id_ne_zero

deleted theorem CategoryTheory.id_nonzero

added theorem CategoryTheory.isIso_of_epi_of_ne_zero

deleted theorem CategoryTheory.isIso_of_epi_of_nonzero

added theorem CategoryTheory.isIso_of_mono_of_ne_zero

deleted theorem CategoryTheory.isIso_of_mono_of_nonzero

added theorem CategoryTheory.kernel_zero_of_ne_zero_from_simple

deleted theorem CategoryTheory.kernel_zero_of_nonzero_from_simple

Modified Mathlib/Combinatorics/Nullstellensatz.lean

added theorem MvPolynomial.combinatorial_nullstellensatz_exists_eval_ne_zero

deleted theorem MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.mem_splitSupport_iff_ne_zero

deleted theorem Finsupp.mem_splitSupport_iff_nonzero

Modified Mathlib/Data/Finsupp/ToDFinsupp.lean

Modified Mathlib/FieldTheory/RatFunc/Valuation.lean

added theorem RatFunc.inftyValuation_of_ne_zero

deleted theorem RatFunc.inftyValuation_of_nonzero

Modified Mathlib/FieldTheory/SeparableDegree.lean

deleted theorem Polynomial.natSepDegree_smul_nonzero

added theorem Polynomial.natSepDegree_smul_of_ne_zero

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

added theorem InnerProductGeometry.angle_neg_self_of_ne_zero

deleted theorem InnerProductGeometry.angle_neg_self_of_nonzero

added theorem InnerProductGeometry.angle_self_neg_of_ne_zero

deleted theorem InnerProductGeometry.angle_self_neg_of_nonzero

Modified Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

added theorem finrank_eq_one_iff_of_ne_zero'

added theorem finrank_eq_one_iff_of_ne_zero

deleted theorem finrank_eq_one_iff_of_nonzero'

deleted theorem finrank_eq_one_iff_of_nonzero

added theorem surjective_of_ne_zero_of_finrank_eq_one

deleted theorem surjective_of_nonzero_of_finrank_eq_one

Modified Mathlib/LinearAlgebra/Projectivization/Basic.lean

modified theorem Projectivization.mk_rep

added theorem Projectivization.rep_ne_zero

deleted theorem Projectivization.rep_nonzero

Modified Mathlib/LinearAlgebra/Projectivization/Independence.lean

Modified Mathlib/LinearAlgebra/Projectivization/PSL/PSL2.lean

Modified Mathlib/MeasureTheory/Group/ModularCharacter.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

added theorem MeasureTheory.integral_pos_of_integrable_nonneg_ne_zero

deleted theorem MeasureTheory.integral_pos_of_integrable_nonneg_nonzero

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

added theorem Continuous.integral_pos_of_hasCompactSupport_nonneg_ne_zero

deleted theorem Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.mass_ne_zero_iff

deleted theorem MeasureTheory.FiniteMeasure.mass_nonzero_iff

added theorem MeasureTheory.FiniteMeasure.restrict_ne_zero_iff

deleted theorem MeasureTheory.FiniteMeasure.restrict_nonzero_iff

Modified Mathlib/MeasureTheory/Measure/Haar/Extension.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_ne_zero

deleted theorem MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero

added theorem MeasureTheory.FiniteMeasure.normalize_eq_of_ne_zero

deleted theorem MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero

added theorem MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_ne_zero

deleted theorem MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_ne_zero

deleted theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero

Modified Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_ne_zero

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_ne_zero

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero

Modified Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean

Modified Mathlib/NumberTheory/Harmonic/Int.lean

Modified Mathlib/NumberTheory/ModularForms/Discriminant.lean

Modified Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

Modified Mathlib/NumberTheory/ModularForms/RamanujanFormula.lean

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

added theorem PadicSeq.norm_ne_zero_of_not_equiv_zero

deleted theorem PadicSeq.norm_nonzero_of_not_equiv_zero

added theorem PadicSeq.not_equiv_zero_const_of_ne_zero

deleted theorem PadicSeq.not_equiv_zero_const_of_nonzero

added theorem PadicSeq.not_limZero_const_of_ne_zero

deleted theorem PadicSeq.not_limZero_const_of_nonzero

Modified Mathlib/RepresentationTheory/AlgebraRepresentation/Basic.lean

Modified Mathlib/RepresentationTheory/FinGroupCharZero.lean

Modified Mathlib/RingTheory/Algebraic/Basic.lean

added theorem IsAlgebraic.exists_coeff_ne_zero_and_aeval_eq_zero

added theorem IsAlgebraic.exists_ne_zero_dvd

added theorem IsAlgebraic.exists_ne_zero_eq_adjoin_mul

deleted theorem IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero

deleted theorem IsAlgebraic.exists_nonzero_dvd

deleted theorem IsAlgebraic.exists_nonzero_eq_adjoin_mul

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/FractionalIdeal/Inverse.lean

added theorem FractionalIdeal.invertible_iff_generator_ne_zero

deleted theorem FractionalIdeal.invertible_iff_generator_nonzero

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

added theorem IsFractional.div_of_ne_zero

deleted theorem IsFractional.div_of_nonzero

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

added theorem Ideal.exists_ne_zero_mem_of_ne_bot

deleted theorem Ideal.exists_nonzero_mem_of_ne_bot

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/SimpleModule/Rank.lean

Modified Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

added theorem WittVector.RecursionBase.solution_ne_zero

deleted theorem WittVector.RecursionBase.solution_nonzero

added theorem WittVector.frobeniusRotation_ne_zero

deleted theorem WittVector.frobeniusRotation_nonzero

Modified Mathlib/RingTheory/WittVector/Identities.lean

added theorem WittVector.FractionRing.p_ne_zero

deleted theorem WittVector.FractionRing.p_nonzero

added theorem WittVector.p_ne_zero

deleted theorem WittVector.p_nonzero

Modified Mathlib/RingTheory/WittVector/Isocrystal.lean

Modified Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean

added theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_head_ne_zero

deleted theorem Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_head

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

added theorem LinearMap.continuous_of_ne_zero_on_open

deleted theorem LinearMap.continuous_of_nonzero_on_open