| Name | Category | Theorems |
|---|
constVAdd π | CompOp | 11 mathmath: constVAdd_apply, constVAdd_add, constVAdd_nsmul, constVAdd_zsmul, constVAdd_zero, ContinuousAffineEquiv.constVAdd_coe, linear_constVAdd, AffineSubspace.pointwise_vadd_eq_map, constVAdd_symm, AffineBasis.coord_vadd, constVAddHom_apply
|
constVAddHom π | CompOp | 1 mathmath: constVAddHom_apply
|
constVSub π | CompOp | 2 mathmath: coe_constVSub, coe_constVSub_symm
|
equivLike π | CompOp | 90 mathmath: coe_symm_toEquiv, AffineIsometryEquiv.coe_mk, coe_toEquiv, sOppSide_map_iff, pointReflection_fixed_iff_of_injective_two_nsmul, AffineIsometryEquiv.coe_symm_toAffineEquiv, coe_mk', constVAdd_apply, coe_mul, continuous_of_finiteDimensional, prodComm_apply, span_eq_top_iff, apply_lineMap, prodAssoc_symm_apply, sSameSide_map_iff, AffineMap.homothety_neg_one_apply, pointReflection_fixed_iff_of_module, ContinuousAffineEquiv.prodComm_symm_apply, ofBijective_apply, pointReflection_involutive, prodAssoc_apply, coe_homothetyUnitsMulHom_apply_symm, coe_constVSub, map_vadd, map_midpoint, coeFn_inj, apply_symm_apply, list_wbtw_map_iff, LinearEquiv.coe_toAffineEquiv, wSameSide_map_iff, injective_pointReflection_left_of_injective_two_nsmul, equivUnitsAffineMap_symm_apply_apply, coe_one, sbtw_pointReflection_of_ne, AffineSubspace.topEquiv_symm_apply_coe, pointReflection_apply_eq_equivPointReflection_apply, pointReflection_midpoint_right, injective_pointReflection_left_of_module, prodCongr_apply, ext_iff, equivUnitsAffineMap_symm_apply_symm_apply, symm_apply_apply, coe_trans, ofLinearEquiv_apply, coe_refl, affineIndependent_set_of_eq_iff, pointReflection_apply, coe_constVSub_symm, AffineSubspace.comap_span, apply_eq_iff_eq_symm_apply, equivUnitsAffineMap_symm_apply_toFun, injective, AffineSubspace.sOppSide_pointReflection, midpoint_eq_iff, refl_apply, coe_toAffineMap, image_symm, AffineSubspace.topEquiv_apply, coe_coe, coe_homothetyUnitsMulHom_apply, apply_eq_iff_eq, midpoint_pointReflection_left, surjective, pointReflection_self, coe_ofEq_apply, list_sbtw_map_iff, wOppSide_map_iff, vaddConst_symm_apply, vaddConst_apply, coe_toHomeomorphOfFiniteDimensional_symm, ContinuousAffineEquiv.coe_symm_toAffineEquiv, coe_mk, AffineIsometryEquiv.coe_vaddConst', ContinuousAffineEquiv.coe_coe, coe_toHomeomorphOfFiniteDimensional, range_eq, sbtw_map_iff, preimage_symm, pointReflection_midpoint_left, wbtw_pointReflection, AffineSubspace.equivMapOfInjective_toFun, AffineSubspace.wOppSide_pointReflection, coeFn_injective, bijective, affineIndependent_iff, trans_apply, ContinuousAffineEquiv.prodAssoc_symm_apply, wbtw_map_iff, midpoint_pointReflection_right, AffineIsometryEquiv.coe_toAffineEquiv
|
equivUnitsAffineMap π | CompOp | 7 mathmath: linear_equivUnitsAffineMap_symm_apply, val_equivUnitsAffineMap_apply, equivUnitsAffineMap_symm_apply_apply, equivUnitsAffineMap_symm_apply_symm_apply, equivUnitsAffineMap_symm_apply_toFun, val_inv_equivUnitsAffineMap_apply, equivUnitsAffineMap_symm_apply_invFun
|
group π | CompOp | 19 mathmath: coe_homothetyUnitsMulHom_eq_homothetyHom_coe, coe_mul, linear_equivUnitsAffineMap_symm_apply, coe_homothetyUnitsMulHom_apply_symm, inv_def, val_equivUnitsAffineMap_apply, constVAdd_nsmul, constVAdd_zsmul, mul_def, equivUnitsAffineMap_symm_apply_apply, coe_one, linearHom_apply, equivUnitsAffineMap_symm_apply_symm_apply, equivUnitsAffineMap_symm_apply_toFun, coe_homothetyUnitsMulHom_apply, val_inv_equivUnitsAffineMap_apply, equivUnitsAffineMap_symm_apply_invFun, one_def, constVAddHom_apply
|
homothetyUnitsMulHom π | CompOp | 3 mathmath: coe_homothetyUnitsMulHom_eq_homothetyHom_coe, coe_homothetyUnitsMulHom_apply_symm, coe_homothetyUnitsMulHom_apply
|
instCoeAffineMap π | CompOp | β |
instCoeOutEquiv π | CompOp | β |
linear π | CompOp | 21 mathmath: linear_vaddConst, AffineIsometryEquiv.linear_eq_linear_isometry, AffineSubspace.linear_topEquiv, linear_equivUnitsAffineMap_symm_apply, linear_prodAssoc, linear_ofEq, map_vadd, linear_symm, linear_toAffineMap, linear_refl, linear_ofLinearEquiv, coe_linear, linearHom_apply, linear_constVAdd, AffineSubspace.linear_equivMapOfInjective, linear_mk', linear_prodCongr, linear_ofBijective, AffineIsometryEquiv.norm_map, map_vadd', linear_prodComm
|
linearHom π | CompOp | 1 mathmath: linearHom_apply
|
mk' π | CompOp | 2 mathmath: coe_mk', linear_mk'
|
ofBijective π | CompOp | 3 mathmath: ofBijective_apply, linear_ofBijective, ofBijective.symm_eq
|
ofLinearEquiv π | CompOp | 4 mathmath: linear_ofLinearEquiv, ofLinearEquiv_refl, ofLinearEquiv_apply, ofLinearEquiv_trans_ofLinearEquiv
|
pointReflection π | CompOp | 21 mathmath: pointReflection_fixed_iff_of_injective_two_nsmul, AffineIsometryEquiv.pointReflection_toAffineEquiv, AffineMap.homothety_neg_one_apply, pointReflection_fixed_iff_of_module, pointReflection_involutive, toEquiv_pointReflection, injective_pointReflection_left_of_injective_two_nsmul, sbtw_pointReflection_of_ne, pointReflection_apply_eq_equivPointReflection_apply, pointReflection_midpoint_right, injective_pointReflection_left_of_module, pointReflection_apply, AffineSubspace.sOppSide_pointReflection, midpoint_eq_iff, midpoint_pointReflection_left, pointReflection_self, pointReflection_midpoint_left, wbtw_pointReflection, AffineSubspace.wOppSide_pointReflection, pointReflection_symm, midpoint_pointReflection_right
|
prodAssoc π | CompOp | 4 mathmath: ContinuousAffineEquiv.prodAssoc_toAffineEquiv, prodAssoc_symm_apply, prodAssoc_apply, linear_prodAssoc
|
prodComm π | CompOp | 4 mathmath: prodComm_apply, ContinuousAffineEquiv.prodComm_toAffineEquiv, prodComm_symm, linear_prodComm
|
prodCongr π | CompOp | 5 mathmath: coe_prodCongr, prodCongr_apply, prodCongr_symm, linear_prodCongr, ContinuousAffineEquiv.prodCongr_toAffineEquiv
|
refl π | CompOp | 16 mathmath: symm_trans_self, self_trans_symm, linear_refl, constVAdd_zero, ofLinearEquiv_refl, coe_refl, refl_apply, coe_refl_to_affineMap, AffineIsometryEquiv.toAffineEquiv_refl, trans_refl, refl_trans, symm_refl, ofEq_rfl, toEquiv_refl, ContinuousAffineEquiv.toAffineEquiv_refl, one_def
|
toAffineMap π | CompOp | 25 mathmath: sOppSide_map_iff, coe_homothetyUnitsMulHom_eq_homothetyHom_coe, toAffineMap_inj, AffineSubspace.comap_symm, sSameSide_map_iff, toAffineMap_mk, AffineSubspace.map_symm, AffineSubspace.isometryEquivMap.toAffineMap_eq, linear_toAffineMap, val_equivUnitsAffineMap_apply, coe_trans_to_affineMap, wSameSide_map_iff, coe_linear, coe_prodCongr, toAffineMap_injective, AffineSubspace.pointwise_vadd_eq_map, AffineSubspace.comap_span, coe_toAffineMap, coe_refl_to_affineMap, coe_coe, EuclideanGeometry.Sphere.orthRadius_map, AffineBasis.coord_vadd, wOppSide_map_iff, val_inv_equivUnitsAffineMap_apply, ContinuousAffineEquiv.toContinuousAffineMap_toAffineMap
|
toEquiv π | CompOp | 16 mathmath: coe_symm_toEquiv, coe_toEquiv, ContinuousAffineEquiv.toEquiv_symm, toEquiv_symm, ContinuousAffineEquiv.coe_toEquiv, toEquiv_injective, toEquiv_pointReflection, ContinuousAffineEquiv.toEquiv_refl, ContinuousAffineEquiv.coe_symm_toEquiv, ContinuousAffineEquiv.continuous_toFun, ContinuousAffineEquiv.continuous_invFun, toEquiv_inj, map_vadd', equivUnitsAffineMap_symm_apply_invFun, toEquiv_refl, ofBijective.symm_eq
|
trans π | CompOp | 11 mathmath: symm_trans_self, self_trans_symm, constVAdd_add, trans_assoc, coe_trans_to_affineMap, mul_def, coe_trans, ofLinearEquiv_trans_ofLinearEquiv, trans_refl, refl_trans, trans_apply
|
vaddConst π | CompOp | 5 mathmath: linear_vaddConst, AffineIsometryEquiv.vaddConst_toAffineEquiv, vaddConst_symm_apply, vaddConst_apply, AffineIsometryEquiv.coe_vaddConst'
|