Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 08:42 ac76eb37

View on Github →

feat(algebra/star/unitary): lemmas about group_with_zero (#11493)

Estimated changes

Modified src/algebra/star/unitary.lean

added theorem unitary.coe_div

added theorem unitary.coe_inv

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 def unitary.to_units

added theorem unitary.to_units_injective