OAI/Algebra/AffineCancellation/BezoutFrame.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ComplexCancellation.BezoutFrame.exists_frame line 11

   Source documentation

   Principalization of an SL₂/diagonal-torus point over a Euclidean domain. This supplies the invariant-localization frame over the slice polynomial ring.

   theorem exists_frame {R : Type*} [EuclideanDomain R] (x y z : R)
       (h : x*y = z*(z+1)) :
       ∃ a d b c : R, a*b = x ∧ d*c = y ∧ d*b = z ∧ a*c-d*b = 1 := by
   …

   Mentions: OAI.ComplexCancellation.x