mathlib

68626536 - feat(linear_algebra/dual): more about dual annihilator, some refactoring, and documentation (#17521)

feat(linear_algebra/dual): more about dual annihilator, some refactoring, and documentation (#17521) * Extend documentation with descriptions of main definitions and results. * Move `linear_map.dual_map` earlier in the file and redefine it to use `module.transpose`. * `fintype` -> `set.finite` for `module.dual_bases`. * Rename `submodule.dual_annihilator_comap` to `submodule.dual_coannihilator`. * Add galois correspondence and coinsertion for `submodule.dual_annihilator`; replace proofs using standard GC lemmas. * Add `submodule.dual_pairing` and `submodule.dual_copairing` for bilinear forms that are nondegenerate for subspaces. * Add missing isomorphisms associated to these. * Generalize `f.dual_map.range = f.ker.dual_annihilator` to vector spaces of arbitrary dimension. * Add lemmas for facts such as `(W ⊓ W').dual_annihilator = W.dual_annihilator ⊔ W'.dual_annihilator`. Thanks to Junyan Xu for the generalization to `dual_quot_equiv_dual_annihilator`.