OAI/AlgebraicGeometry/CommutingDerivations/OrdinaryExtraMain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The all-dimensional family may be chosen with the additional n-4 directions literally equal to the ordinary ambient coordinate partials.

  1. def OAI.AbhyankarSathaye.CommutingDerivations.withOrdinaryExtras line 13
  2. def OAI.AbhyankarSathaye.CommutingDerivations.extraClearingExponent line 20
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_with_ordinary_extras line 25

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Fin, HSub.hSub, Derivation, Complex, MvPolynomial, Finsupp, And, Eq, HAdd.hAdd, OAI.AbhyankarSathaye.extendedF, OAI.AbhyankarSathaye.CommutingDerivations.LocallyNilpotent, LinearIndependent, Iff, Membership.mem, Subalgebra, Algebra.adjoin and 11 more

    Proof uses: Algebra, OAI.AbhyankarSathaye.CommutingDerivations.ExtendedLocalizedAmbient, OAI.AbhyankarSathaye.CommutingDerivations.LocalizedAmbient, OAI.AbhyankarSathaye.R, Submonoid.powers, OAI.AbhyankarSathaye.CommutingDerivations.ambientC, OAI.AbhyankarSathaye.CommutingDerivations.extendedAlgebra, IsScalarTower, OAI.AbhyankarSathaye.CommutingDerivations.extendedScalarTower, IsLocalization.Away, OAI.AbhyankarSathaye.CommutingDerivations.extended_isLocalization, OAI.AbhyankarSathaye.CommutingDerivations.extendedAmbientParameter, id, AlgHom, OAI.AbhyankarSathaye.CommutingDerivations.extendedLocAlgHom, Function.Injective, OAI.AbhyankarSathaye.CommutingDerivations.extendedParameter_localization_injective, IsUnit, IsLocalization.Away.algebraMap_isUnit, RingHom and 45 more

    123 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: ComparatorChallenges/CommutingDerivations.lean:54 (same statement text; different proof or body). Qualify references as OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_with_ordinary_extras@path.

    Tactic trace: 30 steps

    Open to load the checked before-and-after goal states.