Commit 2024-05-16 14:20 dc75ecfa

View on Github →

refactor: Turn Algebra.IsAlgebraic and Algebra.IsIntegral into classes (#12761) As discussed on Zulip, this PR replaces the current definition of Algebra.IsAlgebraic and Algebra.IsIntegral with classes. The following main changes are required:

  • Since a class must be a structure, we can't identify Algebra.IsAlgebraic R A with ∀ (x : A), IsAlgebraic R x. Either use the projection .isAlgebraic, or use the new definition Algebra.IsAlgebraic.isAlgebraic which leaves the proof implicit. Idem for integral.
  • Turn Algebra.IsAlgebraic and Algebra.IsIntegral arguments into instance implicits; turn theorems with those as the conclusion into instances.
  • Algebra.IsAlgebraic is now protected, like Algebra.IsIntegral. The spelling Algebra.IsAlgebraic.isAlgebraic x and Algebra.IsIntegral.isIntegral x to prove an element x is algebraic/integral is kind of ugly, do you have better suggestions?

Estimated changes

modified theorem IsAlgClosure.ofAlgebraic
deleted theorem Normal.isAlgebraic
modified theorem Normal.isIntegral
modified theorem Field.finSepDegree_eq
modified theorem eq_separableClosure_iff
modified theorem separableClosure.eq_bot_iff
modified theorem separableClosure_le_iff
deleted theorem IsSeparable.isAlgebraic
deleted def Algebra.IsAlgebraic
modified theorem Algebra.IsIntegral.finite
added theorem Algebra.isIntegral_def
deleted theorem Module.End.isIntegral
modified theorem isIntegral_trans
modified theorem isIntegral_localization