OAI/Topology/CoarseAssembly/CoefficientFamilyMultiplier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual multiplier underlying a coefficient-family boundary

  1. def OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyMultiplier line 22
  2. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyMultiplier_value line 31
  3. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyMultiplier_selfAdjoint line 39
  4. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyMultiplier_defect line 49
  5. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientFamilyBoundary_eq_multiplier line 62