def SingularPoints.IsNonsingularPoint (k : Type u_2) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k n) : Prop

A point $P$ on the algebraic set $V(f_1, \dots, f_m)$ of expected dimension $d$ is nonsingular if the Jacobian matrix at $P$ has rank $n - d$.

def SingularPoints.IsSingularPoint (k : Type u_2) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k n) : Prop

A singular point on $V(f_1, \dots, f_m)$ is one where the Jacobian fails to achieve the expected rank $n - d$.

def SingularPoints.IsSmoothVariety (k : Type u_2) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : Prop

A variety is smooth (of dimension $d$) if every point of $V(f_1, \dots, f_m)$ is nonsingular, i.e. the Jacobian has rank $n - d$ everywhere.

def SingularPoints.IsNonsingularPointIntrinsic (k : Type u_2) [Field k] (n m d : ℕ) (V : Set (AffineSpace_k k n)) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (_hVar : IsAffineVariety k n V) (_hgen : Ideal.span (Set.range f) = idealOfAlgebraicSet V) (_hdim : HasDimension k n V d) (P : AffineSpace_k k n) : Prop

Intrinsic nonsingularity: a point $P \in V$ is nonsingular relative to chosen generators $f_i$ of the ideal of $V$ when the Jacobian has rank $n - d$.

def SingularPoints.IsSingularPointIntrinsic (k : Type u_2) [Field k] (n m d : ℕ) (V : Set (AffineSpace_k k n)) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (_hVar : IsAffineVariety k n V) (_hgen : Ideal.span (Set.range f) = idealOfAlgebraicSet V) (_hdim : HasDimension k n V d) (P : AffineSpace_k k n) : Prop

Intrinsic singularity: a point $P \in V$ is singular when the Jacobian of a chosen generating set of $I(V)$ has rank different from $n - d$.

def SingularPoints.IsSmoothVarietyIntrinsic (k : Type u_2) [Field k] (n m d : ℕ) (V : Set (AffineSpace_k k n)) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (_hVar : IsAffineVariety k n V) (_hgen : Ideal.span (Set.range f) = idealOfAlgebraicSet V) (_hdim : HasDimension k n V d) : Prop

An intrinsic notion of smoothness: every point of $V$ is nonsingular with respect to a chosen generating set of the ideal $I(V)$.