The Lean 4 theorem `hasZeroDeficiencyOn_top_of_symmetric` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization
ProvedBookProof.NavierStokesFlow.hasZeroDeficiencyOn_top_of_symmetrictimepiece
The Lean 4 theorem hasZeroDeficiencyOn_top_of_symmetric in the ChapterNavierStokesFlow chapter of the timepiece formalization.
Preamble
-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.hasZeroDeficiencyOn_top_of_symmetric
import Mathlib
import Definitions.Def_ChapterNavierStokesFlow
open BookProof.NavierStokesFlow
open scoped BigOperators Matrix Kronecker ComplexOrder TensorProduct
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.NavierStokesFlow.hasZeroDeficiencyOn_top_of_symmetric (H : F →ₗ[ℂ] F) (hsym : H.IsSymmetric) :
HasZeroDeficiencyOn (⊤ : Submodule ℂ F) (restrictToTop H) := by sorrySource