How to avoid making an arg explicit in def.

Stream: mathlib4

[Michail Karatarakis]

I have this code :

import Mathlib.NumberTheory.NumberField.Discriminant

open NumberField Embeddings FiniteDimensional

noncomputable section

variable {K : Type*} [Field K] [NumberField K]

def h := (finrank ℚ K)

def σ : Fin (finrank ℚ K) ≃ (K →+* ℂ) := sorry

Is it possible to alter the definition of h to enable writing def σ : Fin (h) ≃ (K →+* ℂ) := sorry without needing an explicitK for h ?

[Yaël Dillies]

local notation h := finrank ℚ K?

[Antoine Chambert-Loir]

(Unrelated with the actual question, h is usually the class number of the number field, not its degree (which could be d or r).)

[Notification Bot]

This topic was moved here from #maths > How to avoid making an arg explicit in def. by Eric Wieser.