def definition def or abbrev

`Radical`

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

formal statement (Lean)

  20def Radical {n : ℕ} (α : Vec n) : Set (Vec n) :=

Definition body.

  21  { v | dot α v = 0 }
  22
  23/-- The affine leaves orthogonal to the active direction. -/

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

add_mem_Radical in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
affineShift_mem_LevelSet in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
mem_Radical_iff in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
preserves_own_leaf_iff_mem_Radical in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
quadraticHessian_eq_zero_iff in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
radical_integrable_by_affine_leaves in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
smul_mem_Radical in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
sub_mem_Radical in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
zero_mem_Radical in IndisputableMonolith.Cost.Ndim.RadicalDistribution decl_use
omega_eighthundredforty in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
radical_eighthundredforty in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use

Lean names referenced from this declaration's body.