MinimalTensorKernelFaithful.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A star homomorphism on a minimal tensor product is faithful if its kernel contains no nonzero elementary tensor. Pure-state excision detects an elementary tensor in every nonzero kernel.

def OAI.WeakPureInfiniteness.tensorHomKernel line 20
theorem OAI.WeakPureInfiniteness.minimalTensor_injective_of_elementary_kernel line 38
Source documentation
No assumption of nuclearity is needed for this zero-kernel assertion.
```
theorem minimalTensor_injective_of_elementary_kernel
    (q : MinimalTensor A B →⋆ₙₐ[ℂ] D)
    (hq : ∀ a b, q (minimalElementary a b) = 0 → minimalElementary a b = 0) :
    Function.Injective q := by
…
```
Mentions: OAI.WeakPureInfiniteness.MinimalTensor, OAI.WeakPureInfiniteness.minimalElementary