Commit 2024-10-17 11:36 dc528566
View on Github →feat(Algebraize): Fix algebraize tactic (#17839)
This fixes algebraize tactic to work better when it is pointing to a (possibly custom) constructor/theorem giving the algebra property from the corresponding ringhom property. As an application we apply this to the new IsStandardSmooth, RingHom property.