OAI/Analysis/OperatorAlgebra/LpAlgebraicInstances.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of the algebraic structures used by the concrete L² space and by the abstract normed-space estimates.

  1. lemma OAI.WeakPureInfiniteness.lp_addCommGroup_from_normed line 13
  2. lemma OAI.WeakPureInfiniteness.lp_addCommMonoid_from_normed line 18