Commit 2023-01-09 09:40 b6c42e59

View on Github →

feat: port Algebra.Star.Basic (#1331)

Estimated changes

added theorem IsUnit.star
added theorem MulOpposite.op_star
added theorem MulOpposite.unop_star
added theorem Ring.inverse_star
added theorem RingHom.star_apply
added theorem RingHom.star_def
added theorem Units.coe_star
added theorem Units.coe_star_inv
added theorem conjugate_le_conjugate
added theorem conjugate_nonneg'
added theorem conjugate_nonneg
added theorem eq_star_iff_eq_star
added theorem eq_star_of_eq_star
added theorem isUnit_star
added def starAddEquiv
added def starMulAut
added def starMulEquiv
added def starRingAut
added def starRingEnd
added theorem starRingEnd_apply
added theorem starRingEnd_self_apply
added def starRingEquiv
added def starRingOfComm
added theorem star_bit0
added theorem star_bit1
added theorem star_div'
added theorem star_div
added theorem star_eq_iff_star_eq
added theorem star_eq_zero
added theorem star_id_of_comm
added theorem star_injective
added theorem star_intCast
added theorem star_inv'
added theorem star_inv
added theorem star_invOf
added theorem star_mul'
added theorem star_mul_self_nonneg'
added theorem star_mul_self_nonneg
added theorem star_natCast
added theorem star_ne_zero
added theorem star_neg
added theorem star_nsmul
added theorem star_one
added theorem star_pow
added theorem star_ratCast
added theorem star_star
added theorem star_sub
added theorem star_zero
added theorem star_zpow
added theorem star_zpow₀
added theorem star_zsmul