Commit 2024-08-21 18:42 00e250b4

View on Github →

chore(Algebra/Prod): add Prod.mk_one_one (#15922)

  • Normalize (1, 1) and (0, 0) to 1 and 0, respectively.
  • Add Polynomial.mul_coeff_one Moves:
  • PerfectClosure.mk_zero_zero -> PefectClosure.mk_zero
  • PerfectClosure.mk_zero -> PerfectClosure.mk_zero_right

Estimated changes

added theorem Prod.mk_one_one
modified theorem PerfectClosure.mk_zero
modified theorem Submodule.prod_bot