Commit 2022-12-04 13:00 9f19a1b9

View on Github →

feat: port algebra.ring.basic (#830)

  • copy and obvious corrections
  • fix
  • using autoimplicits
  • reinserted map_bit0
  • linter
  • import adhoc file
  • fix imports
  • compiles
  • satisfy linter
  • fix: move stuff out of Algebra.RIng.Basic_old
  • fix tests

Estimated changes

added def AddHom.mulLeft
added def AddHom.mulRight
deleted theorem Int.cast_Nat_cast
deleted theorem Int.cast_eq_cast_iff_Nat
deleted theorem Int.cast_id
deleted theorem Int.natAbs_cast
deleted theorem Int.ofNat_eq_cast
deleted theorem Nat.cast_commute
deleted theorem Nat.cast_id
deleted theorem Nat.cast_mul
deleted theorem Nat.cast_pow
deleted theorem coe_nat_zsmul
added theorem inv_neg'
added theorem map_bit0
added theorem pred_ne_self
added theorem succ_ne_self
deleted theorem zpow_coe_nat
added theorem Int.cast_Nat_cast
added theorem Int.cast_id
added theorem Int.natAbs_cast
added theorem Int.ofNat_eq_cast
added theorem coe_nat_zsmul
added theorem zpow_coe_nat
added theorem Nat.cast_commute
added theorem Nat.cast_id
added theorem Nat.cast_mul
added theorem Nat.cast_pow