@[simp]
theorem
LinearMap.BilinForm.dualBasis_reindex
{K : Type u_1}
{V : Type u_2}
[Field K]
[AddCommGroup V]
[Module K V]
{ι : Type u_3}
{ι' : Type u_4}
[DecidableEq ι]
[DecidableEq ι']
[Finite ι]
[Finite ι']
(B : LinearMap.BilinForm K V)
(hB : B.Nondegenerate)
(b : Module.Basis ι K V)
(e : ι ≃ ι')
: