OAI/AlgebraicGeometry/CommutingDerivations/FamilyFromLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of a commuting, locally nilpotent, linearly independent family from a relative localization equivalence and a coefficient-intersection identity.

  1. theorem OAI.AbhyankarSathaye.CommutingDerivations.exists_commuting_family_of_localization line 20