Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-09 09:40
b6c42e59
View on Github →
feat: port Algebra.Star.Basic (
#1331
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Star/Basic.lean
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_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
def
starSemigroupOfComm
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