@[implicit_reducible]

noncomputable instance L2InnerProductSpace.instSeminormedAddCommGroupSmoothForm (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] [CompactSpace M] [MeasurableSpace M] (k : ℕ) : SeminormedAddCommGroup (HodgeStarMathlib.SmoothForm n M k)

$L^2$ seminorm structure on smooth $k$-forms on a compact complex $n$-manifold, induced by the pointwise Hermitian inner product and the volume form.

@[implicit_reducible]

noncomputable instance L2InnerProductSpace.instInnerProductSpaceSmoothForm (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℂ (Fin n)) M] [IsManifold (modelWithCornersSelf ℂ (EuclideanSpace ℂ (Fin n))) ⊤ M] [CompactSpace M] [MeasurableSpace M] (k : ℕ) : InnerProductSpace ℝ (HodgeStarMathlib.SmoothForm n M k)

$L^2$ inner product structure on smooth $k$-forms, $\langle \alpha, \beta \rangle = \int_M \alpha \wedge \star \bar\beta$, used to define the formal adjoints $\bar\partial^*$ and $\partial^*$.