English
The map dualDistribInvOfBasis is compatible with changing the bases: if b=b1 and c=c1 and b2,c2 are another pair of bases, equality holds between the two induced maps.
Русский
Отображение dualDistribInvOfBasis совместимо с заменой базисов: при b=b1, c=c1 и другой паре базисов b2,c2 тождество сохраняется между соответствующими отображениями.
LaTeX
$$$$ dualDistribInvOfBasis b c = dualDistribInvOfBasis b' c' \\quad \\text{при } b=b', c=c'. $$$$
Lean4
theorem dualDistrib_dualDistribInvOfBasis_right_inverse (b : Basis ι R M) (c : Basis κ R N) :
comp (dualDistribInvOfBasis b c) (dualDistrib R M N) = LinearMap.id :=
by
apply (b.dualBasis.tensorProduct c.dualBasis).ext
rintro ⟨i, j⟩
simp only [Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp, Function.comp_apply, dualDistribInvOfBasis_apply,
dualDistrib_apply, Basis.coord_apply, Basis.repr_self, id_coe, id_eq]
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
· simp
all_goals { intros; simp [*] at *
}
