chore: more adaptations for lean4#5542 (#17655)

In [lean4#5542](leanprover/lean4#5542) we are deprecating `inductive ... :=`, `structure ... :=`, and `class ... :=` for their `... where` counterparts. Continuation of #17564.

Author: kmill

Diff for: Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

@@ -26,7 +26,7 @@ equivalences acts transitively on the set of nonzero vectors.
 registers that continuous linear forms on `E` separate points of `E`. -/
 @[mk_iff separatingDual_def]
 class SeparatingDual (R V : Type*) [Ring R] [AddCommGroup V] [TopologicalSpace V]
-    [TopologicalSpace R] [Module R V] : Prop :=
+    [TopologicalSpace R] [Module R V] : Prop where
   /-- Any nonzero vector can be mapped by a continuous linear map to a nonzero scalar. -/
   exists_ne_zero' : ∀ (x : V), x ≠ 0 → ∃ f : V →L[R] R, f x ≠ 0
 

Diff for: Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

@@ -235,7 +235,7 @@ variable {f : α × β → ℚ → ℝ}
 conditions are the same, but the limit properties of `IsRatCondKernelCDF` are replaced by
 limits of integrals. -/
 structure IsRatCondKernelCDFAux (f : α × β → ℚ → ℝ) (κ : Kernel α (β × ℝ)) (ν : Kernel α β) :
-    Prop :=
+    Prop where
   measurable : Measurable f
   mono' (a : α) {q r : ℚ} (_hqr : q ≤ r) : ∀ᵐ c ∂(ν a), f (a, c) q ≤ f (a, c) r
   nonneg' (a : α) (q : ℚ) : ∀ᵐ c ∂(ν a), 0 ≤ f (a, c) q
@@ -425,7 +425,7 @@ respect to `ν` if it is measurable, tends to 0 at -∞ and to 1 at +∞ for all
 `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ` and for all
 measurable sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal`. -/
 structure IsCondKernelCDF (f : α × β → StieltjesFunction) (κ : Kernel α (β × ℝ)) (ν : Kernel α β) :
-    Prop :=
+    Prop where
   measurable (x : ℝ) : Measurable fun p ↦ f p x
   integrable (a : α) (x : ℝ) : Integrable (fun b ↦ f (a, b) x) (ν a)
   tendsto_atTop_one (p : α × β) : Tendsto (f p) atTop (𝓝 1)

Diff for: Mathlib/RingTheory/Algebraic.lean

@@ -48,11 +48,11 @@ def Subalgebra.IsAlgebraic (S : Subalgebra R A) : Prop :=
 variable (R A)
 
 /-- An algebra is algebraic if all its elements are algebraic. -/
-protected class Algebra.IsAlgebraic : Prop :=
+protected class Algebra.IsAlgebraic : Prop where
   isAlgebraic : ∀ x : A, IsAlgebraic R x
 
 /-- An algebra is transcendental if some element is transcendental. -/
-protected class Algebra.Transcendental : Prop :=
+protected class Algebra.Transcendental : Prop where
   transcendental : ∃ x : A, Transcendental R x
 
 variable {R A}

Diff for: Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean

@@ -29,7 +29,7 @@ variable [Algebra R A] (R)
 variable (A)
 
 /-- An algebra is integral if every element of the extension is integral over the base ring. -/
-protected class Algebra.IsIntegral : Prop :=
+protected class Algebra.IsIntegral : Prop where
   isIntegral : ∀ x : A, IsIntegral R x
 
 variable {R A}