Namespace LinearEquiv 2 theorems
- Eventual dimension inequality for φ-stable subspace pairs
LinearEquiv.exists_forall_finrank_inf_map_pow_add_finrank_inf_le0 below · cited by 2 · depth 13 - Equivariant dual isomorphism descends to the modules
LinearEquiv.exists_equiv_forall_dual_eq_comp_symm_and_comp_eq_of_dual_equiv_forall_comp_eq0 below · cited by 1 · depth 23