CornerUnitaryExtension.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite signed groups in a proper matrix corner act as the identity on its complementary subspace. These algebraic identities retain that action.

theorem OAI.KadisonKastler.add_complement_mul line 20
Source documentation
Adding the complementary identity respects multiplication on the range of a nonunital star homomorphism.
```
theorem add_complement_mul (φ : A →⋆ₙₐ[ℂ] B) (a b : A) :
    (φ a + (1 - φ 1)) * (φ b + (1 - φ 1)) = φ (a * b) + (1 - φ 1) := by
…
```
def OAI.KadisonKastler.cornerUnitaryExtension line 32
Source documentation
A unitary in a represented corner is a unitary on the whole space after adding the complementary identity.
```
def cornerUnitaryExtension (φ : A →⋆ₙₐ[ℂ] B) : unitary A →* unitary B where
…
```
theorem OAI.KadisonKastler.cornerUnitaryExtension_coe line 47