OAI/Geometry/RCD/Sobolev/GammaColumnMixed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mixed energy pairings with a finite coordinate column

  1. theorem OAI.RegularPointCoordinates.localGamma_column_right line 13

    Distinct definitions of this name: OAI/Geometry/RCD/Harmonic/RadialLinearCombination.lean:32 (different declaration text). Qualify references as OAI.RegularPointCoordinates.localGamma_column_right@path.