Commit 2023-01-09 16:13 c7304b78

View on Github →

feat: Port Algebra.Star.Unitary (#1436)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Star/Unitary.lean

added theorem unitary.coe_div

added theorem unitary.coe_inv

added theorem unitary.coe_mul_star_self

added theorem unitary.coe_neg

added theorem unitary.coe_star

added theorem unitary.coe_star_mul_self

added theorem unitary.coe_zpow

added theorem unitary.mem_iff

added theorem unitary.mem_iff_self_mul_star

added theorem unitary.mem_iff_star_mul_self

added theorem unitary.mul_star_self

added theorem unitary.mul_star_self_of_mem

added theorem unitary.star_eq_inv'

added theorem unitary.star_eq_inv

added theorem unitary.star_mem

added theorem unitary.star_mem_iff

added theorem unitary.star_mul_self

added theorem unitary.star_mul_self_of_mem

added def unitary.toUnits

added theorem unitary.to_units_injective

added def unitary