Def RingHom.testProperty1

Modification history

2025-06-19 05:50
MathlibTest/algebraize.lean
feat(Tactic/Algebraize): Allow the `algebraize` tactic to use lemmas which don't (directly) mention RingHom (#24661) …
Deleted RingHom.testProperty1View on Github →
2024-10-04 10:12
test/algebraize.lean
feat(Tactic/Algebraize): add algebraize tactic (#16217) …
Added RingHom.testProperty1View on Github →