Theoremsadd_apply, coe_hom, comp_apply, exists_kernelι_eq, forget₂_map, hom_apply, instLinearMapClassHomSubtypeModuleCatLinearMapIdCarrierOfMulActionV_classFieldTheory, eq_sum_smul_of, instAddMonoidHomClassHomSubtypeModuleCatLinearMapIdCarrierTrivialV_classFieldTheory, instMulActionHomClassHomSubtypeModuleCatLinearMapIdCarrierTrivialV_classFieldTheory, leftRegularHom_eq_ρReg, leftRegularHom_of, nontrivial_iff_nontrivial, of_apply, of_apply_eq_one, of_def, of_eq_ρ_of_one, ε_comp_ρ, ε_comp_ρ_apply, ε_epi, ε_eq_sum, ε_eq_sum', ε_of, ε_of_one, ρ_apply, ρ_apply_of, ρ_apply₃, ρ_apply₃_self_mul, ρ_comp_lsingle, leftRegularHomEquiv_symm_comp, mkIso_hom_hom, mkIso_inv_hom, of_ρ', richards, smul_apply, sub_apply, zero_apply, ρ_apply, ρ_mul_eq_comp, norm_ofIsTrivial, range_eq_span | 41 |