How do I use strong mathematical induction?TT

Stream: lean4

[东禹]

How do I use strong mathematical induction？TT

[东禹]

theorem simultaneous_diagonalization
    (matrix_family : Set (Matrix (Fin n) (Fin n) K))
    (nonempty : ∃ A, A ∈ matrix_family)
    (commutes : ∀ A ∈ matrix_family, ∀ B ∈ matrix_family, A * B = B * A)
    (each_diagonalizable : ∀ A ∈ matrix_family, Diagonalizable A) :
    ∃ (S : Matrix (Fin n) (Fin n) K),
      S.det ≠ 0 ∧  -- Invertible
      ∀ A ∈ matrix_family,
        ∃ (diag : Fin n → K),
          S⁻¹ * A * S = diagonal diag := by

[东禹]

How do I use strong mathematical induction on n? I only learned weak mathematical induction in MIL.

[Aaron Liu]

docs#Nat.strongRec

[东禹]

Thank you！！！