Commit 2024-10-04 10:12 58523222

feat(Tactic/Algebraize): add algebraize tactic (#16217) This PR adds the algebraize tactic, which automatically adds Algebra, and if possible IsScalarTower instances corresponding to RingHoms given as arguments to the tactic. It will also search through the local context for RingHom properties of those RingHoms, and add the corresponding Algebra properties. The RingHom properties which have a corresponding Algebra property should be tagged using the algebraize attribute, which is also given in this PR. That attribute takes a name of a the corresponding Algebra property as an attribute, or of a constructor for such a property (this is needed when the proof of the corresponding Algebra property is not just given by a term the RingHom property). For examples of its usage, see the files in RingTheory/ which are also modified in this PR. Most of this tactic was created during the AIM workshop "Formalizing algebraic geometry" in June 2024. Co-authored by: Johan Commelin, Nick Kuhn, Arend Mellendijk, Christian Merten, Adam Topaz (there might have been more, please let me know if you are not in this list!)