Commit 2025-01-03 23:29 f87a1350

View on Github →

chore(Algebra): Improve attribute generation (#20451)

  • Teach to_additive about oneLE -> nonneg and square -> even
  • Make simps lemma generated for the carrier projection consistently coe_*
  • Clarify some documentation Moves:
  • \*_coe -> coe_\* where generated by @[simps]
    • IsOpenMap.functor_obj_coe -> IsOpenMap.coe_functor_obj
    • AlgebraicGeometry.Scheme.Hom.opensRange_coe -> AlgebraicGeometry.Scheme.Hom.coe_opensRange

Estimated changes

modified theorem Submonoid.mem_oneLE