OAI/Analysis/Nuclearity/UnitalIdealQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A local unital structure on the closed-ideal quotient.

  1. abbrev OAI.WeakPureInfiniteness.unitalIdealQuotientStructure line 14
  2. theorem OAI.WeakPureInfiniteness.UnitalIdealQuotient.mk_one line 26
  3. def OAI.WeakPureInfiniteness.UnitalIdealQuotient.quotientHom line 32
  4. theorem OAI.WeakPureInfiniteness.UnitalIdealQuotient.quotientHom_eq_zero_iff line 40