Theoremscoe_codRestrict, coe_range, injective_codRestrict, map_adjoin, map_adjoin_singleton, mem_equalizer, mem_range, mem_range_self, range_comp, range_comp_le_range, subsingleton, subtype_comp_codRestrict, adjoin_eq, adjoin_eq_span, adjoin_eq_starClosure_adjoin, adjoin_induction, adjoin_le, adjoin_le_centralizer_centralizer, adjoin_le_iff, adjoin_mono, adjoin_toNonUnitalSubalgebra, coe_bot, coe_iInf, coe_inf, coe_sInf, coe_top, comap_top, commute_of_mem_adjoin_of_forall_mem_commute, commute_of_mem_adjoin_self, commute_of_mem_adjoin_singleton_of_commute, eq_top_iff, gc, iInf_toNonUnitalSubalgebra, inf_toNonUnitalSubalgebra, map_bot, map_iInf, map_inf, map_sup, map_top, mem_adjoin_of_mem, mem_bot, mem_iInf, mem_inf, mem_sInf, mem_sup_left, mem_sup_right, mem_top, mul_mem_sup, range_eq_top, range_id, sInf_toNonUnitalSubalgebra, self_mem_adjoin_singleton, span_eq_toSubmodule, star_self_mem_adjoin_singleton, star_subset_adjoin, subset_adjoin, toNonUnitalSubalgebra_bot, toNonUnitalSubalgebra_eq_top, top_toNonUnitalSubalgebra, center_eq_top, center_toNonUnitalSubalgebra, centralizer_le, centralizer_toNonUnitalSubalgebra, centralizer_univ, coe_add, coe_center, coe_centralizer, coe_centralizer_centralizer, coe_comap, coe_copy, coe_eq_zero, coe_iSup_of_directed, coe_map, coe_mul, coe_neg, coe_prod, coe_smul, coe_sub, coe_toNonUnitalSubalgebra, coe_toNonUnitalSubring, coe_zero, copy_eq, ext, ext_iff, gc_map_comap, iSupLift_comp_inclusion, iSupLift_inclusion, iSupLift_mk, iSupLift_of_mem, inclusion_inclusion, inclusion_injective, inclusion_mk, inclusion_right, inclusion_self, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMulForallForallStar, instIsScalarTower, instIsScalarTower', instIsTorsionFree, instNoZeroDivisors, instNonUnitalSubringClass, instNonUnitalSubsemiringClass, instSMulCommClass, instSMulCommClass', instSMulMemClass, instStarMemClass, map_id, map_injective, map_le, map_map, map_mono, map_toNonUnitalSubalgebra, mem_carrier, mem_center_iff, mem_centralizer_iff, mem_comap, mem_map, mem_prod, mem_toNonUnitalSubalgebra, mem_toNonUnitalSubring, ofClass_carrier, prod_inf_prod, prod_mono, prod_toNonUnitalSubalgebra, prod_top, range_val, star_mem', subsingleton_of_subsingleton, toNonUnitalSubalgebra_inj, toNonUnitalSubalgebra_injective, toNonUnitalSubalgebra_le_iff, toNonUnitalSubalgebra_subtype, toNonUnitalSubalgebra_toNonUnitalStarSubalgebra, toNonUnitalSubring_inj, toNonUnitalSubring_injective, toSubring_subtype, val_inclusion, coe_subtype, subtype_apply, subtype_injective, coe_star, coe_starClosure, coe_toNonUnitalStarSubalgebra, mem_starClosure, mem_star_iff, mem_toNonUnitalStarSubalgebra, starClosure_eq_adjoin, starClosure_le, starClosure_le_iff, starClosure_mono, starClosure_toNonUnitalSubalgebra, star_adjoin_comm, star_mem_star_iff, star_mono, toNonUnitalStarSubalgebra_toNonUnitalSubalgebra, ofInjective'_apply, ofLeftInverse'_apply, ofLeftInverse'_symm_apply, instStarModule | 158 |