`BookProof.LorentzGroup.delta_mul_closed` : ∀ x ∈ Delta, ∀ y ∈ Delta, x * y ∈ Delta
ProvedBookProof.LorentzGroup.delta_mul_closedtheoremstimepiece
Prove the following Lean 4 theorem from ChapterLorentzGroup.
BookProof.LorentzGroup.delta_mul_closed : ∀ x ∈ Delta, ∀ y ∈ Delta, x * y ∈ Delta
Formalization note: Lean 4 identifier BookProof.LorentzGroup.delta_mul_closed.
Preamble
-- Generated from ChapterLorentzGroup.lean — theorem BookProof.LorentzGroup.delta_mul_closed import Mathlib import Definitions.Def_ChapterLorentzGroup open BookProof.LorentzGroup open Matrix
Formal statement
theorem BookProof.LorentzGroup.delta_mul_closed : ∀ x ∈ Delta, ∀ y ∈ Delta, x * y ∈ Delta := by sorry