OAI/Analysis/BoundedHochschild/SubalgebraModules.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Right module identities from subalgebra unitary invariance.

  1. def OAI.BoundedHochschild.unitaryInclusion line 21
  2. lemma OAI.BoundedHochschild.coe_unitaryInclusion line 26
  3. lemma OAI.BoundedHochschild.continuous_unitaryInclusion line 29
  4. lemma OAI.BoundedHochschild.right_module_subalgebra line 35