No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
36abbrev ScalarField (siteCount : ℕ) := Fin siteCount → ℝ
proof body
Definition body.
37
used by (29)
From the project-wide theorem graph. These declarations reference this one in their body.
-
backwardDiff
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
conservativeTransportField
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
CoreNSOperator
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
forwardDiff
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
IncompressibleNSOperator
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
scalarLaplacian
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
total_conservativeTransportField_zero
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
kinetic_action
in IndisputableMonolith.Relativity.Fields.Integration
decl_use
-
kinetic_nonneg
in IndisputableMonolith.Relativity.Fields.Integration
decl_use
-
potential_action
in IndisputableMonolith.Relativity.Fields.Integration
decl_use
-
add
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
add_comm
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
deriv_add
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
deriv_smul
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
directional_deriv
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
eval
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
field_squared
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
field_squared_nonneg
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
gradient
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
gradient_squared
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
gradient_squared_minkowski
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
ScalarField
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
smul
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
smul_zero
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
zero
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
ScalarField
in IndisputableMonolith.Relativity.Geometry.Tensor
decl_use
-
expand_action_around_FRW
in IndisputableMonolith.Relativity.GW.ActionExpansion
decl_use
-
RefreshField
in IndisputableMonolith.Relativity.ILG.Action
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
ScalarField
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
ScalarField
in IndisputableMonolith.Relativity.Geometry.Tensor
decl_use