def definition def or abbrev

`IsSymmetric`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  21def IsSymmetric (T : Tensor 0 2) : Prop :=

Definition body.

  22  ∀ x up low, T x up low = T x up (fun i => if i.val = 0 then low 1 else low 0)
  23
  24/-- Symmetrisation: T_(μν) = 1/2 (T_μν + T_νμ). -/

From the project-wide theorem graph. These declarations reference this one in their body.

bilinear_family_forced in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
F_symmetric_of_P_symmetric in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
IsSymmetric in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
P_symmetric_from_F_symmetric in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
symmetry_and_normalization_constrain_P in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
log_aczel_data_of_laws in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use
J_is_unique_cost_under_logic in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
laws_of_logic_imply_dalembert_hypotheses in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
non_contradiction_and_scale_imply_reciprocal in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
operative_derived_cost_symmetric in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.DirectProof decl_use

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
IsSymmetric in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
Tensor in IndisputableMonolith.Relativity.Geometry.Tensor decl_use