Commit 2025-07-03 08:00 ccc5b6cd

View on Github →

feat(Tactic/Ring/NamePolyVars): A command for naming variables in polynomial rings (#26652)

Estimated changes

Modified Counterexamples/CliffordAlgebraNotInjective.lean

deleted theorem Q60596.X0_X1_X2_notMem_kIdeal

added theorem Q60596.X_Y_Z_notMem_kIdeal

deleted theorem Q60596.mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem

added theorem Q60596.mul_self_mem_kIdeal_of_X_Y_Z_mul_mem

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean

modified theorem WeierstrassCurve.Jacobian.comp_fin3

modified theorem WeierstrassCurve.Jacobian.equation_some

modified theorem WeierstrassCurve.Jacobian.fin3_def_ext

modified theorem WeierstrassCurve.Jacobian.nonsingularLift_some

modified theorem WeierstrassCurve.Jacobian.nonsingular_some

modified theorem WeierstrassCurve.Jacobian.polynomialY_eq

modified theorem WeierstrassCurve.Jacobian.polynomialZ_eq

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean

modified theorem WeierstrassCurve.Projective.comp_fin3

modified theorem WeierstrassCurve.Projective.equation_some

modified theorem WeierstrassCurve.Projective.fin3_def_ext

modified theorem WeierstrassCurve.Projective.nonsingularLift_some

modified theorem WeierstrassCurve.Projective.nonsingular_some

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Ring/NamePolyVars.lean

added def Mathlib.Tactic.elabNameVariablesOver

Modified scripts/noshake.json