AffineMap

📁 Source: Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Statistics

Metric	Count
Definitions AffineMap, comp, const, distribMulAction, fst, homothety, homothetyAffine, homothetyHom, id, instAdd, instAddCommGroup, instAddTorsor, instFunLike, instInhabited, instModule, instMonoid, instNeg, instSub, instZero, lineMap, linear, linearHom, mk', mulAction, pi, prod, prodMap, proj, snd, toConstProdLinearMap, toFun, toAffineMap, «term_→ᵃ[_]_»	33
Theorems add_linear, apply_lineMap, coeFn_injective, coe_add, coe_comp, coe_const, coe_fst, coe_homothety, coe_homothetyAffine, coe_homothetyHom, coe_id, coe_lineMap, coe_mk, coe_mk', coe_mul, coe_neg, coe_one, coe_prod, coe_prodMap, coe_smul, coe_snd, coe_sub, coe_zero, comp_apply, comp_assoc, comp_id, comp_lineMap, comp_linear, congr_arg, congr_fun, const_apply, const_linear, decomp, decomp', ext, ext_iff, ext_linear, ext_linear_iff, fst_lineMap, fst_linear, homothety_add, homothety_apply, homothety_apply_same, homothety_def, homothety_eq_iff_of_mul_eq_one, homothety_eq_lineMap, homothety_inj, homothety_injective, homothety_linear, homothety_mul, homothety_mul_apply, homothety_one, homothety_zero, id_apply, id_comp, id_linear, image_uIcc, image_vsub_image, isCentralScalar, left_vsub_lineMap, lineMap_anti, lineMap_apply, lineMap_apply', lineMap_apply_module, lineMap_apply_module', lineMap_apply_one, lineMap_apply_one_sub, lineMap_apply_ring, lineMap_apply_ring', lineMap_apply_zero, lineMap_eq_left_iff, lineMap_eq_lineMap_iff, lineMap_eq_right_iff, lineMap_injective, lineMap_lineMap_left, lineMap_lineMap_right, lineMap_linear, lineMap_mono, lineMap_same, lineMap_same_apply, lineMap_symm, lineMap_vadd_apply, lineMap_vadd_lineMap, lineMap_vsub_left, lineMap_vsub_lineMap, lineMap_vsub_right, linearHom_apply, linearMap_vsub, linear_bijective_iff, linear_eq_zero_iff_exists_const, linear_injective_iff, linear_surjective_iff, map_vadd, map_vadd', mk'_linear, neg_linear, nonempty, pi_apply, pi_comp, pi_eq_zero, pi_ext_nonempty, pi_ext_nonempty', pi_ext_zero, pi_lineMap_apply, pi_linear, pi_zero, prodMap_apply, prodMap_linear, prod_apply, prod_linear, proj_apply, proj_linear, proj_pi, right_vsub_lineMap, smul_linear, snd_lineMap, snd_linear, sub_linear, toConstProdLinearMap_apply, toConstProdLinearMap_symm_apply, toFun_eq_coe, vadd_apply, vadd_linear, vsub_apply, vsub_linear, zero_linear, combo_affine_apply, coe_toAffineMap, toAffineMap_linear	129
Total	162

AffineMap

Definitions

Name	Category	Theorems
comp 📖	CompOp	17 math math: coe_comp, comp_assoc, comp_apply, proj_pi, AffineEquiv.coe_trans_to_affineMap, comp_linear, Affine.Simplex.map_comp, AffineSubspace.map_map, AffineSubspace.comap_comap, pi_comp, comp_lineMap, AffineBasis.coord_vadd, lineMap_symm, homothety_mul, AffineBasis.coord_smul, comp_id, id_comp
const 📖	CompOp	10 math math: const_linear, const_apply, AffineSubspace.signedInfDist_eq_const_of_mem, coe_const, toConstProdLinearMap_symm_apply, homothety_zero, linear_eq_zero_iff_exists_const, lineMap_same, homothety_def, homothety_add
distribMulAction 📖	CompOp	2 math math: homothety_def, homothety_add
fst 📖	CompOp	2 math math: coe_fst, fst_linear
homothety 📖	CompOp	47 math math: eventually_homothety_image_subset_of_finite_subset_interior, homothety_continuous, homothety_one, Convex.closure_subset_interior_image_homothety_of_one_lt, Finset.homothety_affineCombination, homothety_neg_one_apply, homothety_mem, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, dist_center_homothety, homothety_apply_same, eventually_homothety_mem_of_mem_interior, homothety_eq_iff_of_mul_eq_one, dist_homothety_self, nndist_center_homothety, dist_self_homothety, MeasureTheory.euclideanHausdorffMeasure_homothety_image, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, EuclideanGeometry.oangle_homothety, MeasureTheory.hausdorffMeasure_homothety_image, dist_homothety_center, homothety_linear, EuclideanGeometry.angle_homothety, homothety_invOf_two, EuclideanGeometry.inversion_mul, homothety_zero, homothety_isOpenMap, homothety_apply, coe_homothetyHom, coe_homothetyAffine, AffineEquiv.coe_homothetyUnitsMulHom_apply, Convex.subset_interior_image_homothety_of_one_lt, homothety_def, nndist_homothety_center, homothety_inj, homothety_add, homothety_mul, Convex.closure_subset_image_homothety_interior_of_one_lt, homothety_inv_two, MeasureTheory.hausdorffMeasure_homothety_preimage, homothety_injective, nndist_self_homothety, nndist_homothety_self, homothety_one_half, homothety_eq_lineMap, homothety_mul_apply, coe_homothety, MeasureTheory.Measure.addHaar_image_homothety
homothetyAffine 📖	CompOp	1 math math: coe_homothetyAffine
homothetyHom 📖	CompOp	2 math math: AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, coe_homothetyHom
id 📖	CompOp	14 math math: Affine.Simplex.map_id, homothety_one, id_apply, coe_id, id_linear, AffineEquiv.coe_refl_to_affineMap, AffineSubspace.map_id, AffineSubspace.comap_id, homothety_def, AffineSubspace.inclusion_rfl, homothety_add, comp_id, AffineIsometry.id_toAffineMap, id_comp
instAdd 📖	CompOp	3 math math: add_linear, toConstProdLinearMap_symm_apply, coe_add
instAddCommGroup 📖	CompOp	23 math math: AffineEquiv.congrLeftₗ_symm_apply, ContinuousAffineMap.vadd_toAffineMap, instFinite, vadd_linear, vsub_apply, AffineEquiv.arrowCongrₗ_symm_apply, finrank_eq, AffineEquiv.congrLeft_apply, toConstProdLinearMap_apply, AffineEquiv.congrLeft_symm_apply, toConstProdLinearMap_symm_apply, vsub_linear, lineMap_apply', vadd_apply, AffineEquiv.arrowCongrₗ_apply, coe_homothetyAffine, AffineEquiv.linear_arrowCongr, ContinuousAffineMap.vsub_toAffineMap, homothety_def, AffineEquiv.arrowCongr_symm_apply, homothety_add, AffineEquiv.arrowCongr_apply, AffineEquiv.congrLeftₗ_apply
instAddTorsor 📖	CompOp	15 math math: ContinuousAffineMap.vadd_toAffineMap, vadd_linear, vsub_apply, AffineEquiv.congrLeft_apply, AffineEquiv.congrLeft_symm_apply, vsub_linear, lineMap_apply', vadd_apply, coe_homothetyAffine, AffineEquiv.linear_arrowCongr, ContinuousAffineMap.vsub_toAffineMap, homothety_def, AffineEquiv.arrowCongr_symm_apply, homothety_add, AffineEquiv.arrowCongr_apply
instFunLike 📖	CompOp	515 math math: AffineSubspace.wOppSide_lineMap_right, coe_comp, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.affineCombination_mem_closedInterior_iff, Affine.Simplex.altitudeFoot_restrict, lineMap_apply_module, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, hasStrictDerivAt_lineMap, Finset.affineCombination_vsub, lineMap_vsub_left, Finset.affineCombination_affineCombinationSingleWeights, restrict.bijective, ContinuousAffineMap.lineMap_apply', smooth_barycentric_coord, coe_smul, Filter.Tendsto.lineMap, hasDerivAtFilter, Finset.affineCombination_apply_eq_lineMap_sum, Finset.centroid_eq_affineCombination_fintype, curveIntegrable_segment, right_lt_lineMap_iff_one_lt, pi_lineMap_apply, StarConvex.affine_preimage, dist_sq_lineMap_lineMap_of_inner_eq_zero, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, Wbtw.map, Convex.lineMap_mem, ContinuousAffineMap.coe_mk, Finset.affineCombination_sdiff_sub, eqOn_affineSpan, eventually_homothety_image_subset_of_finite_subset_interior, sbtw_iff_mem_image_Ioo_and_ne, Wbtw.right_mem_image_Ici_of_left_ne, lineMap_rev_mem_affineSpan_pair, hasDerivWithinAt, Convex.affine_image, Affine.Simplex.restrict_map_restrict, AffineEquiv.arrowCongrEquiv_symm_apply, signedDist_right_congr, lineMap_le_map_iff_slope_le_slope_right, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, AffineSubspace.subtype_apply, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, AffineSubspace.sOppSide_lineMap_left, span_eq_top_of_surjective, lineMap_inv_two, slope_comp, ContinuousAffineMap.coe_lineMap_eq, AffineBasis.coord_apply_ne, AffineIndependent.affineCombination_eq_iff_eq, Convex.mapsTo_lineMap, homothety_continuous, signedDist_left_congr, congr_arg, StrictConvex.affine_image, EuclideanGeometry.Cospherical.inclusion_iff, curveIntegralFun_segment, signedDist_triangle, EuclideanGeometry.Cospherical.inclusion, Finset.affineCombination_apply_const, wbtw_lineMap_iff, nndist_right_lineMap, sbtw_iff_left_ne_and_right_mem_image_Ioi, comp_apply, AffineEquiv.apply_lineMap, Affine.Simplex.circumradius_restrict, nndist_left_lineMap, Affine.Simplex.medial_restrict, AffineBasis.coord_apply, norm_sub_le_mul_volume_of_norm_lineDeriv_le, Convex.closure_subset_interior_image_homothety_of_one_lt, signedDist_le_dist, AffineSubspace.coe_subtypeₐᵢ, StarConvex.affine_image, affineSpan_eq_affineSpan_lineMap_units, lineMap_mono_endpoints, Affine.Simplex.excenter_eq_affineCombination, signedDist_apply_apply, Function.Injective.list_sbtw_map_iff, AffineEquiv.congrLeftₗ_symm_apply, lineMap_injective, Finset.homothety_affineCombination, AffineSubspace.map_mk', Affine.Simplex.centroid_map, map_lt_lineMap_iff_slope_lt_slope_right, affineCombination_mem_affineSpan_pair, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo, Finset.affineCombination_congr, Affine.Simplex.face_restrict, differentiableWithinAt, Polygon.edgeSet_eq_image_edgePath, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, homothety_neg_one_apply, Affine.Simplex.interior_restrict, Finset.affineCombination_eq_linear_combination, toFun_eq_coe, image_openSegment, apply_lineMap, linear_injective_iff, hasDerivAt_lineMap, Finset.sum_smul_const_vsub_eq_vsub_affineCombination, left_vsub_lineMap, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg, hasDerivWithinAt_lineMap, pi_apply, mem_affineSpan_iff_eq_affineCombination, coe_mk, curveIntegral_segment, AffineBasis.toMatrix_apply, decomp', lineMap_vsub_right, lineMap_continuous, ext_iff, AffineEquiv.ofBijective_apply, Finset.affineCombination_of_eq_one_of_eq_zero, affineCombination_mem_affineSpan, dist_affineCombination_lt_of_strictConvexSpace, dist_lineMap_left, signedDist_eq_zero_of_orthogonal, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, lineMap_lt_right_iff_lt_one, Affine.Simplex.interior_map, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, lineMap_le_lineMap_iff_of_lt', lineMap_strict_mono_endpoints, ContinuousOn.lineMap, Sbtw.right_mem_image_Ioi, ContinuousAffineMap.coe_toAffineMap, right_lt_lineMap_iff_lt, Affine.Simplex.altitude_restrict_eq_comap_subtype, AffineSubspace.signedInfDist_eq_signedDist_of_mem, lineMap_mem_openSegment, homothety_mem, Finset.attach_affineCombination_coe, eq_affineCombination_of_mem_affineSpan_image, proj_apply, id_apply, Finset.map_affineCombination, right_le_lineMap_iff_le, List.exists_map_eq_of_sorted_nonempty_iff_sbtw, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, signedDist_zero, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, dist_center_homothety, lineMap_lineMap_right, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, homothety_apply_same, const_apply, lineMap_mem, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, lineMap_mono, right_vsub_lineMap, coe_id, Wbtw.left_mem_image_Ici_of_right_ne, signedDist_triangle_left, ConcaveOn.comp_affineMap, Sbtw.affineCombination_of_mem_affineSpan_pair, AffineSubspace.wOppSide_lineMap_left, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, sbtw_iff_right_ne_and_left_mem_image_Ioi, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, linearMap_vsub, AffineIsometry.coe_toAffineMap, lineMap_le_left_iff_nonpos, vadd_lineMap, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, eventually_homothety_mem_of_mem_interior, Affine.Simplex.ExcenterExists.excenter_restrict, congr_fun, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, homothety_eq_iff_of_mul_eq_one, hasDerivAt, List.exists_map_eq_of_sorted_nonempty_iff_wbtw, vsub_lineMap, vsub_apply, lineMap_le_right_iff_le, dist_lineMap_right, differentiableAt, AffineBasis.toMatrix_vecMul_coords, AffineEquiv.arrowCongrₗ_symm_apply, map_lt_lineMap_iff_slope_lt_slope_left, MeasureTheory.hausdorffMeasure_lineMap_image, lipschitzWith_of_finiteDimensional, signedDist_smul_of_pos, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, lineMap_apply_module', AffineSubspace.wSameSide_lineMap_left, ContinuousWithinAt.lineMap, signedDist_lineMap_lineMap, AffineBasis.sum_coord_apply_eq_one, Affine.Simplex.exradius_restrict, Finset.affineCombination_map, signedDist_vadd_left_swap, AffineBasis.det_smul_coords_eq_cramer_coords, eq_affineCombination_of_mem_affineSpan_of_fintype, AffineBasis.coord_apply_combination_of_notMem, Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, dist_homothety_self, lineMap_vsub, map_vectorSpan, nndist_center_homothety, coe_const, Finset.affineCombination_indicator_subset, lineMap_eq_lineMap_iff, AffineEquiv.congrLeft_apply, signedDist_vadd_right, AffineSubspace.mem_map, AffineSubspace.mem_map_iff_mem_of_injective, dist_self_homothety, lineMap_lt_left_iff_lt, List.exists_map_eq_of_sorted_iff_sbtw, LinearMap.coe_toAffineMap, Function.Injective.sbtw_map_iff, map_le_lineMap_iff_slope_le_slope_right, map_vadd, coe_fst, image_uIcc, lineMap_vadd_apply, Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.affineCombination_eq_touchpoint_iff, Affine.Simplex.circumcenter_restrict, restrict.injective, Affine.Simplex.height_restrict, AffineSubspace.WSameSide.map, nndist_lineMap_right, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, Finset.affineCombination_apply, linear_surjective_iff, AffineSubspace.subtype_injective, affineCombination_mem_affineSpan_image, signedDist_lineMap_left, lineMap_apply_zero, Finset.affineCombination_affineCombinationLineMapWeights, StrictConvex.affine_preimage, fst_lineMap, AffineSubspace.map_span, MeasureTheory.euclideanHausdorffMeasure_homothety_image, Finset.affineCombination_filter_of_ne, Affine.Simplex.map_comp, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, EuclideanGeometry.oangle_homothety, Function.Injective.sSameSide_map_iff, signedDist_anticomm, AffineSubspace.mem_comap, MeasureTheory.hausdorffMeasure_homothety_image, eq_lineMap_of_dist_eq_mul_of_dist_eq_mul, Affine.Simplex.map_mkOfPoint, derivWithin, lineMap_apply, AffineBasis.coord_apply_eq, AffineBasis.coord_apply_centroid, left_le_lineMap_iff_le, AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype, Affine.Simplex.incenter_restrict, isOpenMap_linear_iff, map_midpoint, mem_affineSpan_pair_iff_exists_lineMap_eq, openSegment_eq_image_lineMap, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, wbtw_iff_right_eq_or_left_mem_image_Ici, signedDist_triangle_right, eq_affineCombination_of_mem_affineSpan, dist_homothety_center, abs_signedDist_eq_dist_iff_vsub_mem_span, Affine.Simplex.affineCombination_mem_interior_face_iff_pos, wbtw_iff_left_eq_or_right_mem_image_Ici, lineMap_lt_map_iff_slope_lt_slope, toConstProdLinearMap_apply, left_lt_lineMap_iff_lt, AffineBasis.toMatrix_inv_vecMul_toMatrix, image_segment, restrict.surjective, Affine.Simplex.inradius_restrict, AffineIndependent.map', restrict.coe_apply, EuclideanGeometry.angle_homothety, lineMap_anti, AffineEquiv.congrLeft_symm_apply, signedDist_neg, AffineSubspace.sSameSide_lineMap_right, homothety_invOf_two, continuous_barycentric_coord, signedDist_vsub_self_rev, lineMap_same_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, lineMap_apply_ring, AffineSubspace.sOppSide_lineMap_right, Affine.Simplex.incenter_eq_affineCombination, signedDist_self, coe_prodMap, Sbtw.left_mem_image_Ioi, signedDist_vsub_self, EuclideanGeometry.inversion_mul, signedDist_smul, Affine.Simplex.centroid_restrict, Function.Injective.sOppSide_map_iff, coe_lineMap, lineMap_le_map_iff_slope_le_slope, lineMap_eq_right_iff, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, ContinuousAffineMap.apply_lineMap, AffineBasis.coords_apply, Affine.Simplex.orthogonalProjectionSpan_restrict, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, lineMap_apply_one, lineMap_apply', Affine.Simplex.setInterior_restrict, vadd_apply, signedDist_smul_of_neg, right_le_lineMap_iff_one_le, lineMap_le_lineMap_iff_of_lt, List.Wbtw.map, List.exists_map_eq_of_sorted_iff_wbtw, Affine.Simplex.excenterWeights_restrict, prod_apply, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, signedDist_vadd_right_swap, AffineEquiv.arrowCongrₗ_apply, decomp, homothety_isOpenMap, Affine.Simplex.median_restrict, isVisible_iff_lineMap, homothety_apply, lineMap_lt_map_iff_slope_lt_slope_left, lineMap_le_right_iff_le_one, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, AffineEquiv.coe_toAffineMap, AffineBasis.surjective_coord, ContinuousMap.Homotopy.affine_apply, linear_bijective_iff, Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype, lineMap_eq_left_iff, Affine.Simplex.closedInterior_restrict, coe_neg, coe_add, Set.InjOn.wbtw_map_iff, dist_left_lineMap, affineCombination_mem_convexHull, signedDist_vadd_left, AddTorsor.convexCombination_eq_affineCombination, lineMap_lt_right_iff_lt, map_le_lineMap_iff_slope_le_slope, coe_homothetyAffine, Finset.weightedVSub_vadd_affineCombination, Affine.Simplex.mongePoint_restrict, snd_lineMap, AffineEquiv.coe_coe, lineMap_one_half, affineCombination_mem_affineSpan_of_nonempty, AffineEquiv.coe_homothetyUnitsMulHom_apply, Affine.Simplex.eulerPoint_restrict, signedDist_apply_linear_apply, AffineSubspace.coe_inclusion_apply, Affine.Simplex.closedInterior_map, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.ExcenterExists.touchpoint_restrict, AffineSubspace.signedInfDist_singleton, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, ext_linear_iff, Affine.Simplex.excenterWeightsUnnorm_restrict, Affine.Simplex.affineCombination_touchpointWeights, Function.Injective.wbtw_map_iff, AffineSubspace.sSameSide_lineMap_left, lineMap_le_left_iff_le, lineMap_lineMap_left, hasStrictDerivAt, continuous_linear_iff, Affine.Simplex.setInterior_map, ContinuousAffineMap.coe_continuousMap_mk, Continuous.lineMap, signedDist_right_lineMap, Finset.attach_affineCombination_of_injective, segment_eq_image_lineMap, lineMap_continuous_uncurry, prodMap_apply, AffineSubspace.WOppSide.map, nndist_lineMap_lineMap, Affine.Simplex.faceOppositeCentroid_map, differentiableOn, AffineSubspace.coe_subtype, comp_lineMap, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, Convex.subset_interior_image_homothety_of_one_lt, ContinuousAt.lineMap, norm_sub_le_mul_volume_of_norm_fderiv_le, sbtw_lineMap_iff, coe_zero, AffineSubspace.wSameSide_lineMap_right, coe_mk', AffineSubspace.signedInfDist_def, ConvexOn.comp_affineMap, signedDist_lineMap_right, affineCombination_eq_centerMass, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, AffineIndependent.exists_affineCombination_eq_smul_eq, AffineEquiv.arrowCongr_symm_apply, isOpenMap_barycentric_coord, Affine.Simplex.signedInfDist_affineCombination, AffineEquiv.arrowCongrEquiv_apply, signedDist_apply, EuclideanGeometry.dist_affineCombination, signedDist_eq_dist_iff_vsub_mem_span, Finset.sum_smul_vsub_const_eq_affineCombination_vsub, nndist_homothety_center, lineMap_apply_ring', Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, map_le_lineMap_iff_slope_le_slope_left, differentiable, homothety_inj, image_convexHull, dist_right_lineMap, AffineBasis.affineCombination_coord_eq_self, affineSegment_image, coe_mul, AffineBasis.coe_coord_of_subsingleton_eq_one, map_lt_lineMap_iff_slope_lt_slope, Set.InjOn.sbtw_map_iff, Finset.sum_smul_vsub_eq_affineCombination_vsub, Finset.lineMap_affineCombination, AffineBasis.coord_apply_combination_of_mem, Convex.closure_subset_image_homothety_interior_of_one_lt, homothety_inv_two, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, coeFn_injective, Function.Injective.wSameSide_map_iff, lineMap_lt_lineMap_iff_of_lt', Path.segment_apply, lipschitzWith_lineMap, lineMap_apply_one_sub, Function.Injective.list_wbtw_map_iff, AffineBasis.linear_combination_coord_eq_self, Affine.Simplex.interior_eq_image_Ioo, abs_signedDist_le_dist, MeasureTheory.hausdorffMeasure_homothety_preimage, lineMap_mono_left, homothety_injective, lineMap_le_map_iff_slope_le_slope_left, AffineEquiv.arrowCongr_apply, AffineSubspace.equivMapOfInjective_toFun, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, AffineIndependent.units_lineMap, lineMap_slope_lineMap_slope_lineMap, EuclideanGeometry.Sphere.secondInter_eq_lineMap, Convex.affine_preimage, lineMap_strict_mono_left, weightedVSub_mem_vectorSpan_pair, coe_sub, signedDist_apply_linear, Affine.Simplex.restrict_map_subtype, antilipschitzWith_of_finiteDimensional, antilipschitzWith_lineMap, image_vsub_image, deriv, lineMap_slope_slope_sub_div_sub, Affine.Simplex.affineCombination_mem_setInterior_iff, EuclideanGeometry.inversion_eq_lineMap, lineMap_mem_affineSpan_pair, AddTorsor.convexComboPair_eq_lineMap, dist_sq_lineMap_of_inner_eq_zero, signedDist_left_lineMap, Affine.Simplex.restrict_map_inclusion, Sbtw.mem_image_Ioo, nndist_self_homothety, AffineSubspace.coe_comap, lineMap_vadd, Finset.centroid_def, lineMap_lt_map_iff_slope_lt_slope_right, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Function.Injective.wOppSide_map_iff, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, left_lt_lineMap_iff_pos, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, coe_snd, vectorSpan_image_eq_submodule_map, nndist_homothety_self, Finset.affineCombination_subtype_eq_filter, coe_one, lineMap_strict_mono_right, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, homothety_one_half, homothety_eq_lineMap, lineMap_vadd_lineMap, convexHull_range_eq_exists_affineCombination, coe_prod, isOpenMap, AffineEquiv.congrLeftₗ_apply, lineMap_lt_lineMap_iff_of_lt, lineMap_mono_right, Affine.Simplex.map_points, dist_lineMap_lineMap, homothety_mul_apply, lineMap_vsub_lineMap, Path.eqOn_extend_segment, nndist_lineMap_left, Convex.combo_affine_apply, signedDist_vadd_vadd, coe_homothety, left_le_lineMap_iff_nonneg, lineMap_lt_left_iff_neg, Affine.Simplex.restrict_points_coe, AffineEquiv.ofBijective.symm_eq, AffineSubspace.mem_map_of_mem, Affine.Simplex.excenterExists_restrict, continuous_of_finiteDimensional, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff, affineIndependent_iff, MeasureTheory.Measure.addHaar_image_homothety, AffineSubspace.coe_map
instInhabited 📖	CompOp	—
instModule 📖	CompOp	15 math math: AffineEquiv.congrLeftₗ_symm_apply, instFinite, AffineEquiv.arrowCongrₗ_symm_apply, finrank_eq, AffineEquiv.congrLeft_apply, toConstProdLinearMap_apply, AffineEquiv.congrLeft_symm_apply, toConstProdLinearMap_symm_apply, lineMap_apply', AffineEquiv.arrowCongrₗ_apply, coe_homothetyAffine, AffineEquiv.linear_arrowCongr, AffineEquiv.arrowCongr_symm_apply, AffineEquiv.arrowCongr_apply, AffineEquiv.congrLeftₗ_apply
instMonoid 📖	CompOp	12 math math: AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, AffineEquiv.val_equivUnitsAffineMap_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, linearHom_apply, coe_homothetyHom, AffineEquiv.val_inv_equivUnitsAffineMap_apply, coe_mul, coe_one, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun
instNeg 📖	CompOp	2 math math: neg_linear, coe_neg
instSub 📖	CompOp	2 math math: sub_linear, coe_sub
instZero 📖	CompOp	4 math math: zero_linear, pi_eq_zero, coe_zero, pi_zero
lineMap 📖	CompOp	173 math math: AffineSubspace.wOppSide_lineMap_right, lineMap_apply_module, hasStrictDerivAt_lineMap, lineMap_vsub_left, ContinuousAffineMap.lineMap_apply', lineMap_linear, Filter.Tendsto.lineMap, Finset.affineCombination_apply_eq_lineMap_sum, curveIntegrable_segment, right_lt_lineMap_iff_one_lt, pi_lineMap_apply, dist_sq_lineMap_lineMap_of_inner_eq_zero, Convex.lineMap_mem, sbtw_iff_mem_image_Ioo_and_ne, Wbtw.right_mem_image_Ici_of_left_ne, lineMap_rev_mem_affineSpan_pair, lineMap_le_map_iff_slope_le_slope_right, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, AffineSubspace.sOppSide_lineMap_left, lineMap_inv_two, ContinuousAffineMap.coe_lineMap_eq, Convex.mapsTo_lineMap, curveIntegralFun_segment, ContinuousAffineMap.lineMap_toAffineMap, wbtw_lineMap_iff, nndist_right_lineMap, sbtw_iff_left_ne_and_right_mem_image_Ioi, AffineEquiv.apply_lineMap, nndist_left_lineMap, norm_sub_le_mul_volume_of_norm_lineDeriv_le, affineSpan_eq_affineSpan_lineMap_units, lineMap_mono_endpoints, lineMap_injective, Finset.homothety_affineCombination, map_lt_lineMap_iff_slope_lt_slope_right, apply_lineMap, hasDerivAt_lineMap, left_vsub_lineMap, hasDerivWithinAt_lineMap, curveIntegral_segment, lineMap_vsub_right, lineMap_continuous, dist_lineMap_left, lineMap_lt_right_iff_lt_one, lineMap_le_lineMap_iff_of_lt', lineMap_strict_mono_endpoints, ContinuousOn.lineMap, Sbtw.right_mem_image_Ioi, right_lt_lineMap_iff_lt, lineMap_mem_openSegment, right_le_lineMap_iff_le, List.exists_map_eq_of_sorted_nonempty_iff_sbtw, lineMap_lineMap_right, lineMap_mem, lineMap_mono, right_vsub_lineMap, Wbtw.left_mem_image_Ici_of_right_ne, AffineSubspace.wOppSide_lineMap_left, sbtw_iff_right_ne_and_left_mem_image_Ioi, lineMap_le_left_iff_nonpos, vadd_lineMap, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, List.exists_map_eq_of_sorted_nonempty_iff_wbtw, vsub_lineMap, lineMap_le_right_iff_le, dist_lineMap_right, map_lt_lineMap_iff_slope_lt_slope_left, MeasureTheory.hausdorffMeasure_lineMap_image, lineMap_apply_module', AffineSubspace.wSameSide_lineMap_left, ContinuousWithinAt.lineMap, signedDist_lineMap_lineMap, lineMap_vsub, lineMap_eq_lineMap_iff, lineMap_lt_left_iff_lt, List.exists_map_eq_of_sorted_iff_sbtw, map_le_lineMap_iff_slope_le_slope_right, lineMap_vadd_apply, nndist_lineMap_right, signedDist_lineMap_left, lineMap_apply_zero, Finset.affineCombination_affineCombinationLineMapWeights, fst_lineMap, eq_lineMap_of_dist_eq_mul_of_dist_eq_mul, lineMap_apply, left_le_lineMap_iff_le, mem_affineSpan_pair_iff_exists_lineMap_eq, openSegment_eq_image_lineMap, wbtw_iff_right_eq_or_left_mem_image_Ici, wbtw_iff_left_eq_or_right_mem_image_Ici, lineMap_lt_map_iff_slope_lt_slope, left_lt_lineMap_iff_lt, lineMap_anti, AffineSubspace.sSameSide_lineMap_right, lineMap_same_apply, lineMap_apply_ring, AffineSubspace.sOppSide_lineMap_right, Sbtw.left_mem_image_Ioi, coe_lineMap, lineMap_le_map_iff_slope_le_slope, lineMap_eq_right_iff, ContinuousAffineMap.apply_lineMap, lineMap_apply_one, lineMap_apply', right_le_lineMap_iff_one_le, lineMap_le_lineMap_iff_of_lt, List.exists_map_eq_of_sorted_iff_wbtw, isVisible_iff_lineMap, lineMap_lt_map_iff_slope_lt_slope_left, lineMap_le_right_iff_le_one, ContinuousMap.Homotopy.affine_apply, lineMap_eq_left_iff, dist_left_lineMap, lineMap_lt_right_iff_lt, map_le_lineMap_iff_slope_le_slope, snd_lineMap, lineMap_one_half, AffineSubspace.sSameSide_lineMap_left, lineMap_le_left_iff_le, lineMap_lineMap_left, lineMap_same, Continuous.lineMap, signedDist_right_lineMap, segment_eq_image_lineMap, lineMap_continuous_uncurry, nndist_lineMap_lineMap, comp_lineMap, ContinuousAt.lineMap, norm_sub_le_mul_volume_of_norm_fderiv_le, sbtw_lineMap_iff, AffineSubspace.wSameSide_lineMap_right, signedDist_lineMap_right, lineMap_symm, lineMap_apply_ring', map_le_lineMap_iff_slope_le_slope_left, dist_right_lineMap, map_lt_lineMap_iff_slope_lt_slope, Finset.lineMap_affineCombination, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, lineMap_lt_lineMap_iff_of_lt', Path.segment_apply, lipschitzWith_lineMap, lineMap_apply_one_sub, Affine.Simplex.interior_eq_image_Ioo, lineMap_mono_left, lineMap_le_map_iff_slope_le_slope_left, AffineIndependent.units_lineMap, lineMap_slope_lineMap_slope_lineMap, EuclideanGeometry.Sphere.secondInter_eq_lineMap, lineMap_strict_mono_left, antilipschitzWith_lineMap, lineMap_slope_slope_sub_div_sub, EuclideanGeometry.inversion_eq_lineMap, lineMap_mem_affineSpan_pair, AddTorsor.convexComboPair_eq_lineMap, dist_sq_lineMap_of_inner_eq_zero, signedDist_left_lineMap, Sbtw.mem_image_Ioo, lineMap_vadd, lineMap_lt_map_iff_slope_lt_slope_right, left_lt_lineMap_iff_pos, lineMap_strict_mono_right, homothety_eq_lineMap, lineMap_vadd_lineMap, lineMap_lt_lineMap_iff_of_lt, lineMap_mono_right, dist_lineMap_lineMap, lineMap_vsub_lineMap, Path.eqOn_extend_segment, nndist_lineMap_left, left_le_lineMap_iff_nonneg, lineMap_lt_left_iff_neg
linear 📖	CompOp	70 math math: lineMap_linear, hasDerivAtFilter, AffineSubspace.map_pointwise_vadd, hasDerivWithinAt, proj_linear, AffineBasis.linear_eq_sumCoords, slope_comp, LinearMap.toAffineMap_linear, signedDist_linear_apply_apply, map_vadd', const_linear, ContinuousAffineMap.coe_mk_contLinear_eq_linear, AffineSubspace.map_mk', linear_injective_iff, AffineSubspace.inclusion_linear, smul_linear, decomp', ContinuousAffineMap.coe_linear_eq_coe_contLinear, AffineIsometry.linear_eq_linearIsometry, vadd_linear, AffineEquiv.linear_toAffineMap, linearMap_vsub, neg_linear, hasDerivAt, map_vectorSpan, id_linear, ContinuousAffineMap.coe_contLinear_eq_linear, AffineEquiv.coe_linear, prod_linear, map_vadd, comp_linear, Finset.affineCombination_linear, linear_surjective_iff, AffineSubspace.subtype_linear, AffineIsometry.norm_map, mk'_linear, derivWithin, add_linear, isOpenMap_linear_iff, prodMap_linear, homothety_linear, toConstProdLinearMap_apply, AffineSubspace.subtypeₐᵢ_linear, AffineSubspace.map_direction, sub_linear, signedDist_linear_apply, vsub_linear, linear_eq_zero_iff_exists_const, linearHom_apply, zero_linear, restrict.linear_aux, decomp, AffineSubspace.linear_equivMapOfInjective, ContinuousAffineMap.coe_contLinear, linear_bijective_iff, signedDist_apply_linear_apply, ext_linear_iff, hasStrictDerivAt, continuous_linear_iff, restrict.linear, snd_linear, EuclideanGeometry.orthogonalProjection_linear, fst_linear, AffineEquiv.linear_ofBijective, signedDist_apply_linear, image_vsub_image, deriv, pi_linear, linear_eqOn_vectorSpan, vectorSpan_image_eq_submodule_map
linearHom 📖	CompOp	2 math math: AffineEquiv.linear_equivUnitsAffineMap_symm_apply, linearHom_apply
mk' 📖	CompOp	2 math math: mk'_linear, coe_mk'
mulAction 📖	CompOp	3 math math: coe_smul, smul_linear, isCentralScalar
pi 📖	CompOp	6 math math: pi_apply, proj_pi, pi_comp, pi_eq_zero, pi_zero, pi_linear
prod 📖	CompOp	4 math math: prod_linear, prod_apply, ContinuousAffineMap.prod_toAffineMap, coe_prod
prodMap 📖	CompOp	5 math math: ContinuousAffineMap.prodMap_toAffineMap, AffineEquiv.coe_prodCongr, prodMap_linear, coe_prodMap, prodMap_apply
proj 📖	CompOp	3 math math: proj_linear, proj_apply, proj_pi
snd 📖	CompOp	2 math math: snd_linear, coe_snd
toConstProdLinearMap 📖	CompOp	2 math math: toConstProdLinearMap_apply, toConstProdLinearMap_symm_apply
toFun 📖	CompOp	4 math math: ContinuousAffineMap.toFun_eq_coe, map_vadd', toFun_eq_coe, ContinuousAffineMap.cont

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap instAdd LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instAdd	—	—
apply_lineMap 📖	mathematical	—	DFunLike.coe AffineMap instFunLike Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne lineMap	—	map_vadd map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass linearMap_vsub
coeFn_injective 📖	mathematical	—	AffineMap DFunLike.coe instFunLike	—	DFunLike.coe_injective
coe_add 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
coe_comp 📖	mathematical	—	DFunLike.coe AffineMap instFunLike comp	—	—
coe_const 📖	mathematical	—	DFunLike.coe AffineMap instFunLike const	—	—
coe_fst 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike fst	—	—
coe_homothety 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—
coe_homothetyAffine 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing addGroupIsAddTorsor AddCommGroup.toAddGroup Ring.toAddCommGroup Semiring.toModule Ring.toSemiring AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instAddCommGroup instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction instAddTorsor instFunLike homothetyAffine homothety	—	smulCommClass_self
coe_homothetyHom 📖	mathematical	—	DFunLike.coe MonoidHom AffineMap CommRing.toRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toMulOneClass instMonoid MonoidHom.instFunLike homothetyHom homothety	—	—
coe_id 📖	mathematical	—	DFunLike.coe AffineMap instFunLike id	—	—
coe_lineMap 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—
coe_mk 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	DFunLike.coe AffineMap instFunLike	—	—
coe_mk' 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike VSub.vsub AddTorsor.toVSub	DFunLike.coe AffineMap instFunLike mk'	—	—
coe_mul 📖	mathematical	—	DFunLike.coe AffineMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_neg 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe AffineMap instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_prod 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike prod Pi.prod	—	—
coe_prodMap 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike prodMap	—	—
coe_smul 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction mulAction Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coe_snd 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike snd	—	—
coe_sub 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
coe_zero 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
comp_apply 📖	mathematical	—	DFunLike.coe AffineMap instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
comp_lineMap 📖	mathematical	—	comp Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne lineMap DFunLike.coe AffineMap instFunLike	—	ext apply_lineMap
comp_linear 📖	mathematical	—	linear comp LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring	—	—
congr_arg 📖	mathematical	—	DFunLike.coe AffineMap instFunLike	—	—
congr_fun 📖	mathematical	—	DFunLike.coe AffineMap instFunLike	—	—
const_apply 📖	mathematical	—	DFunLike.coe AffineMap instFunLike const	—	—
const_linear 📖	mathematical	—	linear const LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero	—	—
decomp 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linear NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_vadd vadd_eq_add add_zero
decomp' 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear addGroupIsAddTorsor AddCommGroup.toAddGroup Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AffineMap instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	decomp map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_add add_sub_cancel_right
ext 📖	—	DFunLike.coe AffineMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AffineMap instFunLike	—	ext
ext_linear 📖	—	linear DFunLike.coe AffineMap instFunLike	—	—	ext linearMap_vsub map_vadd vadd_vsub map_vadd' toFun_eq_coe
ext_linear_iff 📖	mathematical	—	linear DFunLike.coe AffineMap instFunLike	—	AddTorsor.nonempty ext_linear
fst_lineMap 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Prod.instAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike lineMap	—	apply_lineMap
fst_linear 📖	mathematical	—	linear Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup fst LinearMap.fst	—	—
homothety_add 📖	mathematical	—	homothety Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HVAdd.hVAdd AffineMap CommRing.toRing addGroupIsAddTorsor AddCommGroup.toAddGroup instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddCommGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction instAddTorsor SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring distribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring VSub.vsub AddTorsor.toVSub id const	—	smulCommClass_self add_smul vadd_vadd
homothety_apply 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—
homothety_apply_same 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety	—	lineMap_same_apply
homothety_def 📖	mathematical	—	homothety HVAdd.hVAdd AffineMap CommRing.toRing addGroupIsAddTorsor AddCommGroup.toAddGroup instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddCommGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction instAddTorsor SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring distribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring VSub.vsub AddTorsor.toVSub id const	—	—
homothety_eq_iff_of_mul_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety	—	homothety_mul_apply mul_eq_one_comm instIsDedekindFiniteMonoid homothety_one
homothety_eq_lineMap 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne lineMap	—	—
homothety_inj 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety	—	homothety_injective
homothety_injective 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety	—	—
homothety_linear 📖	mathematical	—	linear CommRing.toRing homothety LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.id	—	smulCommClass_self sub_zero add_zero
homothety_mul 📖	mathematical	—	homothety Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing comp CommRing.toRing	—	ext homothety_mul_apply
homothety_mul_apply 📖	mathematical	—	DFunLike.coe AffineMap CommRing.toRing instFunLike homothety Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	SemigroupAction.mul_smul vadd_vsub
homothety_one 📖	mathematical	—	homothety AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing id	—	ext one_smul vsub_vadd
homothety_zero 📖	mathematical	—	homothety MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing const CommRing.toRing	—	ext zero_smul zero_vadd
id_apply 📖	mathematical	—	DFunLike.coe AffineMap instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
id_linear 📖	mathematical	—	linear id LinearMap.id Ring.toSemiring AddCommGroup.toAddCommMonoid	—	—
image_uIcc 📖	mathematical	—	Set.image DFunLike.coe AffineMap DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	linearMap_vsub LinearMap.map_smul map_vadd sub_zero mul_one add_zero Set.image_comp Set.image_mul_const_uIcc Set.image_add_const_uIcc IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
image_vsub_image 📖	mathematical	—	VSub.vsub Set Set.vsub AddTorsor.toVSub AddCommGroup.toAddGroup Set.image DFunLike.coe AffineMap instFunLike LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear	—	Set.ext linearMap_vsub
isCentralScalar 📖	mathematical	—	IsCentralScalar AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction mulAction MulOpposite MulOpposite.instMonoid SMulCommClass.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	SMulCommClass.op_right ext IsCentralScalar.op_smul_eq_smul
left_vsub_lineMap 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	neg_vsub_eq_vsub_rev lineMap_vsub_left smul_neg
lineMap_anti 📖	mathematical	Preorder.toLE	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup instFunLike lineMap	—	neg_le_neg_iff covariant_swap_add_of_covariant_add smul_neg smul_le_smul_of_nonneg_right neg_sub contravariant_swap_add_of_contravariant_add AddGroup.covconv
lineMap_apply 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid VSub.vsub AddTorsor.toVSub	—	—
lineMap_apply' 📖	mathematical	—	DFunLike.coe AffineMap instFunLike addGroupIsAddTorsor AddCommGroup.toAddGroup Ring.toAddCommGroup Semiring.toModule Ring.toSemiring AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instAddCommGroup instModule instAddTorsor lineMap	—	—
lineMap_apply_module 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup instFunLike lineMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toSub AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	smul_sub sub_smul one_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
lineMap_apply_module' 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup instFunLike lineMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubNegMonoid.toSub	—	—
lineMap_apply_one 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	one_smul vsub_vadd
lineMap_apply_one_sub 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_symm comp_apply zero_sub mul_neg mul_one neg_sub sub_add_cancel
lineMap_apply_ring 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_apply_module
lineMap_apply_ring' 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
lineMap_apply_zero 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	zero_smul zero_vadd
lineMap_eq_left_iff 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_eq_lineMap_iff lineMap_apply_zero
lineMap_eq_lineMap_iff 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	lineMap_apply vsub_eq_zero_iff_eq vadd_vsub_vadd_cancel_right sub_smul smul_eq_zero IsDomain.toIsCancelMulZero sub_eq_zero
lineMap_eq_right_iff 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_eq_lineMap_iff lineMap_apply_one
lineMap_injective 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	lineMap_eq_lineMap_iff
lineMap_lineMap_left 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lineMap_apply_one_sub lineMap_lineMap_right
lineMap_lineMap_right 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	vadd_vsub SemigroupAction.mul_smul
lineMap_linear 📖	mathematical	—	linear Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne lineMap LinearMap.smulRight AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.id VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup	—	add_zero
lineMap_mono 📖	mathematical	Preorder.toLE	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup instFunLike lineMap	—	smul_le_smul_of_nonneg_right AddGroup.covconv_swap
lineMap_same 📖	mathematical	—	lineMap const Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	ext lineMap_same_apply
lineMap_same_apply 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	vsub_self smul_zero zero_vadd
lineMap_symm 📖	mathematical	—	lineMap comp Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	comp_lineMap lineMap_apply_one lineMap_apply_zero
lineMap_vadd_apply 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	lineMap_apply vadd_vsub
lineMap_vadd_lineMap 📖	mathematical	—	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	apply_lineMap
lineMap_vsub_left 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	vadd_vsub
lineMap_vsub_lineMap 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap	—	apply_lineMap
lineMap_vsub_right 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_apply_one_sub lineMap_vsub_left
linearHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom AffineMap LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike linearHom linear	—	—
linearMap_vsub 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup AffineMap instFunLike	—	vsub_vadd map_vadd vadd_vsub
linear_bijective_iff 📖	mathematical	—	Function.Bijective DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear AffineMap instFunLike	—	linear_injective_iff linear_surjective_iff
linear_eq_zero_iff_exists_const 📖	mathematical	—	linear LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero const	—	AddTorsor.nonempty ext coe_const vsub_eq_zero_iff_eq linearMap_vsub LinearMap.zero_apply const_linear
linear_injective_iff 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear AffineMap instFunLike	—	AddTorsor.nonempty map_vadd vadd_vsub Equiv.comp_injective Equiv.injective_comp
linear_surjective_iff 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear AffineMap instFunLike	—	AddTorsor.nonempty map_vadd vadd_vsub Equiv.comp_surjective Equiv.surjective_comp
map_vadd 📖	mathematical	—	DFunLike.coe AffineMap instFunLike HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear	—	map_vadd'
map_vadd' 📖	mathematical	—	toFun HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike linear	—	—
mk'_linear 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike VSub.vsub AddTorsor.toVSub	linear mk'	—	—
neg_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap instNeg LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instNeg	—	—
nonempty 📖	mathematical	—	AffineMap	—	Nonempty.map AddTorsor.nonempty
pi_apply 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup instFunLike pi	—	—
pi_comp 📖	mathematical	—	comp Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup pi	—	—
pi_eq_zero 📖	mathematical	—	pi addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor instZero	—	—
pi_ext_nonempty 📖	—	DFunLike.coe AffineMap Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup addGroupIsAddTorsor instFunLike Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	pi_ext_zero Pi.single_zero
pi_ext_nonempty' 📖	—	comp addGroupIsAddTorsor AddCommGroup.toAddGroup Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor LinearMap.toAffineMap LinearMap.single	—	—	pi_ext_nonempty congr_fun
pi_ext_zero 📖	—	DFunLike.coe AffineMap Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup addGroupIsAddTorsor instFunLike Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Pi.instZero	—	—	ext_linear LinearMap.pi_ext map_vadd vadd_right_cancel_iff Pi.single_zero add_zero vadd_eq_add
pi_lineMap_apply 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Pi.addCommGroup Pi.module AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup instFunLike lineMap	—	apply_lineMap
pi_linear 📖	mathematical	—	linear Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup pi LinearMap.pi	—	—
pi_zero 📖	mathematical	—	pi addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap instZero Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor	—	ext
prodMap_apply 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike prodMap	—	—
prodMap_linear 📖	mathematical	—	linear Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup prodMap LinearMap.prodMap	—	—
prod_apply 📖	mathematical	—	DFunLike.coe AffineMap Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike prod	—	—
prod_linear 📖	mathematical	—	linear Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup prod LinearMap.prod	—	—
proj_apply 📖	mathematical	—	DFunLike.coe AffineMap Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup instFunLike proj	—	—
proj_linear 📖	mathematical	—	linear Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup proj LinearMap.proj	—	—
proj_pi 📖	mathematical	—	comp Pi.addCommGroup Pi.module Ring.toSemiring AddCommGroup.toAddCommMonoid Pi.instAddTorsor AddCommGroup.toAddGroup proj pi	—	ext
right_vsub_lineMap 📖	mathematical	—	VSub.vsub AddTorsor.toVSub AddCommGroup.toAddGroup DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instFunLike lineMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	lineMap_apply_one_sub left_vsub_lineMap
smul_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction mulAction LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instSMul DistribMulAction.toDistribSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
snd_lineMap 📖	mathematical	—	DFunLike.coe AffineMap Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Prod.instAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup instFunLike lineMap	—	apply_lineMap
snd_linear 📖	mathematical	—	linear Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid Prod.instAddTorsor AddCommGroup.toAddGroup snd LinearMap.snd	—	—
sub_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap instSub LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instSub	—	—
toConstProdLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroup Prod.instAddCommMonoid LinearMap.addCommMonoid instModule Prod.instModule LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike toConstProdLinearMap instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid linear	—	RingHomInvPair.ids
toConstProdLinearMap_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup Prod.instAddCommMonoid LinearMap.addCommMonoid instAddCommGroup Prod.instModule LinearMap.module instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toConstProdLinearMap instAdd LinearMap.toAffineMap const	—	RingHomInvPair.ids
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe AffineMap instFunLike	—	—
vadd_apply 📖	mathematical	—	DFunLike.coe AffineMap instFunLike HVAdd.hVAdd addGroupIsAddTorsor AddCommGroup.toAddGroup instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddCommGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction instAddTorsor	—	—
vadd_linear 📖	mathematical	—	linear HVAdd.hVAdd AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instAddCommGroup AddAction.toAddSemigroupAction AddTorsor.toAddAction instAddTorsor LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instAdd	—	—
vsub_apply 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup instFunLike VSub.vsub AddTorsor.toVSub instAddCommGroup instAddTorsor	—	—
vsub_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup VSub.vsub AffineMap AddTorsor.toVSub instAddCommGroup instAddTorsor LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instSub	—	—
zero_linear 📖	mathematical	—	linear addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap instZero LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero	—	—

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
combo_affine_apply 📖	mathematical	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction	—	combo_eq_smul_sub_add AffineMap.apply_lineMap

LinearMap

Definitions

Name	Category	Theorems
toAffineMap 📖	CompOp	6 math math: toAffineMap_linear, LinearIsometry.toAffineIsometry_toAffineMap, coe_toAffineMap, AffineMap.toConstProdLinearMap_symm_apply, AffineSubspace.smul_eq_map, AffineBasis.coord_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toAffineMap 📖	mathematical	—	DFunLike.coe AffineMap addGroupIsAddTorsor AddCommGroup.toAddGroup AffineMap.instFunLike toAffineMap LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	—
toAffineMap_linear 📖	mathematical	—	AffineMap.linear addGroupIsAddTorsor AddCommGroup.toAddGroup toAffineMap	—	—

(root)

Definitions

Name	Category	Theorems
AffineMap 📖	CompData	542 math math: AffineSubspace.wOppSide_lineMap_right, AffineMap.coe_comp, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.affineCombination_mem_closedInterior_iff, Affine.Simplex.altitudeFoot_restrict, AffineMap.lineMap_apply_module, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, AffineMap.hasStrictDerivAt_lineMap, Finset.affineCombination_vsub, AffineMap.lineMap_vsub_left, Finset.affineCombination_affineCombinationSingleWeights, AffineMap.restrict.bijective, ContinuousAffineMap.lineMap_apply', smooth_barycentric_coord, AffineMap.coe_smul, AffineMap.nonempty, Filter.Tendsto.lineMap, AffineMap.hasDerivAtFilter, Finset.affineCombination_apply_eq_lineMap_sum, Finset.centroid_eq_affineCombination_fintype, curveIntegrable_segment, right_lt_lineMap_iff_one_lt, AffineMap.pi_lineMap_apply, StarConvex.affine_preimage, AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, dist_sq_lineMap_lineMap_of_inner_eq_zero, Affine.Simplex.restrict_reindex, Affine.Simplex.faceOppositeCentroid_restrict, Wbtw.map, Convex.lineMap_mem, ContinuousAffineMap.coe_mk, Finset.affineCombination_sdiff_sub, AffineMap.eqOn_affineSpan, eventually_homothety_image_subset_of_finite_subset_interior, sbtw_iff_mem_image_Ioo_and_ne, Wbtw.right_mem_image_Ici_of_left_ne, AffineMap.lineMap_rev_mem_affineSpan_pair, AffineMap.hasDerivWithinAt, Convex.affine_image, Affine.Simplex.restrict_map_restrict, AffineEquiv.arrowCongrEquiv_symm_apply, signedDist_right_congr, lineMap_le_map_iff_slope_le_slope_right, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, AffineSubspace.subtype_apply, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, AffineSubspace.sOppSide_lineMap_left, AffineMap.span_eq_top_of_surjective, lineMap_inv_two, AffineMap.slope_comp, ContinuousAffineMap.coe_lineMap_eq, AffineBasis.coord_apply_ne, AffineIndependent.affineCombination_eq_iff_eq, Convex.mapsTo_lineMap, AffineMap.homothety_continuous, signedDist_left_congr, AffineMap.congr_arg, StrictConvex.affine_image, EuclideanGeometry.Cospherical.inclusion_iff, curveIntegralFun_segment, signedDist_triangle, EuclideanGeometry.Cospherical.inclusion, Finset.affineCombination_apply_const, wbtw_lineMap_iff, nndist_right_lineMap, sbtw_iff_left_ne_and_right_mem_image_Ioi, AffineMap.comp_apply, AffineEquiv.apply_lineMap, Affine.Simplex.circumradius_restrict, nndist_left_lineMap, Affine.Simplex.medial_restrict, AffineBasis.coord_apply, norm_sub_le_mul_volume_of_norm_lineDeriv_le, Convex.closure_subset_interior_image_homothety_of_one_lt, signedDist_le_dist, AffineSubspace.coe_subtypeₐᵢ, StarConvex.affine_image, affineSpan_eq_affineSpan_lineMap_units, lineMap_mono_endpoints, Affine.Simplex.excenter_eq_affineCombination, signedDist_apply_apply, Function.Injective.list_sbtw_map_iff, AffineEquiv.congrLeftₗ_symm_apply, AffineMap.lineMap_injective, Finset.homothety_affineCombination, AffineSubspace.map_mk', Affine.Simplex.centroid_map, map_lt_lineMap_iff_slope_lt_slope_right, affineCombination_mem_affineSpan_pair, Affine.Simplex.ninePointCircle_restrict, Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo, Finset.affineCombination_congr, Affine.Simplex.face_restrict, AffineMap.differentiableWithinAt, Polygon.edgeSet_eq_image_edgePath, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, AffineMap.homothety_neg_one_apply, Affine.Simplex.interior_restrict, Finset.affineCombination_eq_linear_combination, AffineMap.toFun_eq_coe, ContinuousAffineMap.vadd_toAffineMap, image_openSegment, AffineMap.apply_lineMap, AffineMap.linear_injective_iff, AffineMap.hasDerivAt_lineMap, Finset.sum_smul_const_vsub_eq_vsub_affineCombination, AffineMap.left_vsub_lineMap, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg, AffineMap.hasDerivWithinAt_lineMap, AffineMap.smul_linear, AffineMap.pi_apply, mem_affineSpan_iff_eq_affineCombination, AffineMap.coe_mk, curveIntegral_segment, AffineBasis.toMatrix_apply, AffineMap.decomp', AffineMap.lineMap_vsub_right, AffineMap.lineMap_continuous, AffineMap.ext_iff, AffineEquiv.ofBijective_apply, Finset.affineCombination_of_eq_one_of_eq_zero, affineCombination_mem_affineSpan, dist_affineCombination_lt_of_strictConvexSpace, dist_lineMap_left, signedDist_eq_zero_of_orthogonal, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, lineMap_lt_right_iff_lt_one, Affine.Simplex.interior_map, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, lineMap_le_lineMap_iff_of_lt', lineMap_strict_mono_endpoints, ContinuousOn.lineMap, Sbtw.right_mem_image_Ioi, ContinuousAffineMap.coe_toAffineMap, right_lt_lineMap_iff_lt, Affine.Simplex.altitude_restrict_eq_comap_subtype, AffineSubspace.signedInfDist_eq_signedDist_of_mem, lineMap_mem_openSegment, AffineMap.homothety_mem, Finset.attach_affineCombination_coe, eq_affineCombination_of_mem_affineSpan_image, AffineMap.proj_apply, AffineMap.id_apply, Finset.map_affineCombination, right_le_lineMap_iff_le, List.exists_map_eq_of_sorted_nonempty_iff_sbtw, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, signedDist_zero, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, dist_center_homothety, AffineMap.lineMap_lineMap_right, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, AffineMap.homothety_apply_same, AffineMap.instFinite, AffineMap.const_apply, AffineMap.lineMap_mem, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, AffineMap.lineMap_mono, AffineMap.vadd_linear, AffineMap.right_vsub_lineMap, AffineMap.coe_id, Wbtw.left_mem_image_Ici_of_right_ne, signedDist_triangle_left, ConcaveOn.comp_affineMap, Sbtw.affineCombination_of_mem_affineSpan_pair, AffineSubspace.wOppSide_lineMap_left, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, sbtw_iff_right_ne_and_left_mem_image_Ioi, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, AffineMap.linearMap_vsub, AffineEquiv.val_equivUnitsAffineMap_apply, AffineIsometry.coe_toAffineMap, lineMap_le_left_iff_nonpos, AffineMap.vadd_lineMap, mem_affineSpan_pair_iff_exists_lineMap_rev_eq, AffineMap.neg_linear, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, eventually_homothety_mem_of_mem_interior, Affine.Simplex.ExcenterExists.excenter_restrict, AffineMap.congr_fun, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, AffineMap.homothety_eq_iff_of_mul_eq_one, AffineMap.hasDerivAt, List.exists_map_eq_of_sorted_nonempty_iff_wbtw, AffineMap.vsub_lineMap, AffineMap.vsub_apply, lineMap_le_right_iff_le, dist_lineMap_right, AffineMap.differentiableAt, AffineBasis.toMatrix_vecMul_coords, AffineEquiv.arrowCongrₗ_symm_apply, map_lt_lineMap_iff_slope_lt_slope_left, MeasureTheory.hausdorffMeasure_lineMap_image, AffineMap.lipschitzWith_of_finiteDimensional, AffineMap.isCentralScalar, signedDist_smul_of_pos, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, AffineMap.lineMap_apply_module', AffineSubspace.wSameSide_lineMap_left, ContinuousWithinAt.lineMap, signedDist_lineMap_lineMap, AffineBasis.sum_coord_apply_eq_one, Affine.Simplex.exradius_restrict, Finset.affineCombination_map, signedDist_vadd_left_swap, AffineBasis.det_smul_coords_eq_cramer_coords, eq_affineCombination_of_mem_affineSpan_of_fintype, AffineBasis.coord_apply_combination_of_notMem, Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, dist_homothety_self, AffineMap.finrank_eq, AffineMap.lineMap_vsub, AffineMap.map_vectorSpan, nndist_center_homothety, AffineMap.coe_const, Finset.affineCombination_indicator_subset, AffineMap.lineMap_eq_lineMap_iff, AffineEquiv.congrLeft_apply, signedDist_vadd_right, AffineSubspace.mem_map, AffineSubspace.mem_map_iff_mem_of_injective, dist_self_homothety, lineMap_lt_left_iff_lt, List.exists_map_eq_of_sorted_iff_sbtw, LinearMap.coe_toAffineMap, Function.Injective.sbtw_map_iff, map_le_lineMap_iff_slope_le_slope_right, AffineMap.map_vadd, AffineMap.coe_fst, AffineMap.image_uIcc, AffineMap.lineMap_vadd_apply, Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.affineCombination_eq_touchpoint_iff, Affine.Simplex.circumcenter_restrict, AffineEquiv.toAffineMap_injective, AffineMap.restrict.injective, Affine.Simplex.height_restrict, AffineSubspace.WSameSide.map, nndist_lineMap_right, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, Finset.affineCombination_apply, AffineMap.linear_surjective_iff, AffineSubspace.subtype_injective, affineCombination_mem_affineSpan_image, signedDist_lineMap_left, AffineMap.lineMap_apply_zero, Finset.affineCombination_affineCombinationLineMapWeights, StrictConvex.affine_preimage, AffineMap.fst_lineMap, AffineSubspace.map_span, MeasureTheory.euclideanHausdorffMeasure_homothety_image, Finset.affineCombination_filter_of_ne, Affine.Simplex.map_comp, MeasureTheory.euclideanHausdorffMeasure_homothety_preimage, EuclideanGeometry.oangle_homothety, Function.Injective.sSameSide_map_iff, signedDist_anticomm, AffineSubspace.mem_comap, MeasureTheory.hausdorffMeasure_homothety_image, eq_lineMap_of_dist_eq_mul_of_dist_eq_mul, Affine.Simplex.map_mkOfPoint, AffineMap.derivWithin, AffineMap.add_linear, AffineMap.lineMap_apply, AffineBasis.coord_apply_eq, AffineBasis.coord_apply_centroid, left_le_lineMap_iff_le, AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype, Affine.Simplex.incenter_restrict, AffineMap.isOpenMap_linear_iff, AffineMap.map_midpoint, mem_affineSpan_pair_iff_exists_lineMap_eq, openSegment_eq_image_lineMap, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, wbtw_iff_right_eq_or_left_mem_image_Ici, signedDist_triangle_right, eq_affineCombination_of_mem_affineSpan, dist_homothety_center, abs_signedDist_eq_dist_iff_vsub_mem_span, Affine.Simplex.affineCombination_mem_interior_face_iff_pos, wbtw_iff_left_eq_or_right_mem_image_Ici, lineMap_lt_map_iff_slope_lt_slope, AffineMap.toConstProdLinearMap_apply, left_lt_lineMap_iff_lt, AffineBasis.toMatrix_inv_vecMul_toMatrix, image_segment, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, AffineIndependent.map', AffineMap.restrict.coe_apply, EuclideanGeometry.angle_homothety, AffineMap.lineMap_anti, AffineEquiv.congrLeft_symm_apply, signedDist_neg, AffineSubspace.sSameSide_lineMap_right, homothety_invOf_two, continuous_barycentric_coord, signedDist_vsub_self_rev, AffineMap.lineMap_same_apply, AffineMap.sub_linear, AffineMap.toConstProdLinearMap_symm_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, AffineMap.lineMap_apply_ring, AffineSubspace.sOppSide_lineMap_right, AffineMap.vsub_linear, Affine.Simplex.incenter_eq_affineCombination, signedDist_self, AffineMap.coe_prodMap, Sbtw.left_mem_image_Ioi, signedDist_vsub_self, EuclideanGeometry.inversion_mul, signedDist_smul, Affine.Simplex.centroid_restrict, Function.Injective.sOppSide_map_iff, AffineMap.coe_lineMap, lineMap_le_map_iff_slope_le_slope, AffineMap.lineMap_eq_right_iff, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, ContinuousAffineMap.apply_lineMap, AffineBasis.coords_apply, Affine.Simplex.orthogonalProjectionSpan_restrict, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, AffineMap.lineMap_apply_one, AffineMap.lineMap_apply', Affine.Simplex.setInterior_restrict, AffineMap.vadd_apply, AffineMap.linearHom_apply, signedDist_smul_of_neg, right_le_lineMap_iff_one_le, lineMap_le_lineMap_iff_of_lt, List.Wbtw.map, List.exists_map_eq_of_sorted_iff_wbtw, Affine.Simplex.excenterWeights_restrict, AffineMap.prod_apply, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, AffineMap.zero_linear, signedDist_vadd_right_swap, AffineEquiv.arrowCongrₗ_apply, AffineMap.decomp, AffineMap.homothety_isOpenMap, Affine.Simplex.median_restrict, isVisible_iff_lineMap, AffineMap.homothety_apply, lineMap_lt_map_iff_slope_lt_slope_left, lineMap_le_right_iff_le_one, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, AffineEquiv.coe_toAffineMap, AffineMap.coe_homothetyHom, AffineBasis.surjective_coord, ContinuousMap.Homotopy.affine_apply, AffineMap.linear_bijective_iff, Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype, AffineMap.lineMap_eq_left_iff, Affine.Simplex.closedInterior_restrict, AffineMap.coe_neg, AffineMap.coe_add, Set.InjOn.wbtw_map_iff, dist_left_lineMap, affineCombination_mem_convexHull, signedDist_vadd_left, AddTorsor.convexCombination_eq_affineCombination, lineMap_lt_right_iff_lt, map_le_lineMap_iff_slope_le_slope, AffineMap.coe_homothetyAffine, Finset.weightedVSub_vadd_affineCombination, Affine.Simplex.mongePoint_restrict, AffineMap.snd_lineMap, AffineEquiv.coe_coe, lineMap_one_half, affineCombination_mem_affineSpan_of_nonempty, AffineEquiv.coe_homothetyUnitsMulHom_apply, Affine.Simplex.eulerPoint_restrict, AffineEquiv.linear_arrowCongr, signedDist_apply_linear_apply, AffineSubspace.coe_inclusion_apply, Affine.Simplex.closedInterior_map, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.ExcenterExists.touchpoint_restrict, AffineSubspace.signedInfDist_singleton, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, AffineMap.ext_linear_iff, Affine.Simplex.excenterWeightsUnnorm_restrict, Affine.Simplex.affineCombination_touchpointWeights, Function.Injective.wbtw_map_iff, AffineSubspace.sSameSide_lineMap_left, lineMap_le_left_iff_le, AffineMap.lineMap_lineMap_left, AffineMap.hasStrictDerivAt, AffineMap.continuous_linear_iff, Affine.Simplex.setInterior_map, ContinuousAffineMap.coe_continuousMap_mk, Continuous.lineMap, signedDist_right_lineMap, Finset.attach_affineCombination_of_injective, AffineMap.pi_eq_zero, segment_eq_image_lineMap, AffineMap.lineMap_continuous_uncurry, ContinuousAffineMap.vsub_toAffineMap, AffineIsometry.toAffineMap_injective, AffineMap.prodMap_apply, AffineSubspace.WOppSide.map, nndist_lineMap_lineMap, Affine.Simplex.faceOppositeCentroid_map, AffineMap.differentiableOn, AffineSubspace.coe_subtype, AffineMap.comp_lineMap, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, Convex.subset_interior_image_homothety_of_one_lt, ContinuousAt.lineMap, norm_sub_le_mul_volume_of_norm_fderiv_le, AffineMap.homothety_def, sbtw_lineMap_iff, AffineMap.coe_zero, AffineSubspace.wSameSide_lineMap_right, AffineMap.coe_mk', AffineSubspace.signedInfDist_def, ConvexOn.comp_affineMap, signedDist_lineMap_right, affineCombination_eq_centerMass, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, AffineIndependent.exists_affineCombination_eq_smul_eq, AffineEquiv.arrowCongr_symm_apply, isOpenMap_barycentric_coord, Affine.Simplex.signedInfDist_affineCombination, AffineEquiv.arrowCongrEquiv_apply, signedDist_apply, EuclideanGeometry.dist_affineCombination, signedDist_eq_dist_iff_vsub_mem_span, Finset.sum_smul_vsub_const_eq_affineCombination_vsub, nndist_homothety_center, AffineEquiv.val_inv_equivUnitsAffineMap_apply, AffineMap.lineMap_apply_ring', Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, map_le_lineMap_iff_slope_le_slope_left, AffineMap.differentiable, AffineMap.homothety_inj, AffineMap.image_convexHull, dist_right_lineMap, AffineBasis.affineCombination_coord_eq_self, affineSegment_image, AffineMap.coe_mul, AffineBasis.coe_coord_of_subsingleton_eq_one, map_lt_lineMap_iff_slope_lt_slope, AffineMap.homothety_add, Set.InjOn.sbtw_map_iff, Finset.sum_smul_vsub_eq_affineCombination_vsub, Finset.lineMap_affineCombination, AffineMap.pi_zero, AffineBasis.coord_apply_combination_of_mem, Convex.closure_subset_image_homothety_interior_of_one_lt, homothety_inv_two, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, AffineMap.coeFn_injective, Function.Injective.wSameSide_map_iff, lineMap_lt_lineMap_iff_of_lt', Path.segment_apply, lipschitzWith_lineMap, AffineMap.lineMap_apply_one_sub, Function.Injective.list_wbtw_map_iff, AffineBasis.linear_combination_coord_eq_self, Affine.Simplex.interior_eq_image_Ioo, abs_signedDist_le_dist, MeasureTheory.hausdorffMeasure_homothety_preimage, lineMap_mono_left, AffineMap.homothety_injective, lineMap_le_map_iff_slope_le_slope_left, AffineEquiv.arrowCongr_apply, AffineSubspace.equivMapOfInjective_toFun, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, AffineIndependent.units_lineMap, lineMap_slope_lineMap_slope_lineMap, EuclideanGeometry.Sphere.secondInter_eq_lineMap, Convex.affine_preimage, lineMap_strict_mono_left, weightedVSub_mem_vectorSpan_pair, AffineMap.coe_sub, signedDist_apply_linear, Affine.Simplex.restrict_map_subtype, AffineMap.antilipschitzWith_of_finiteDimensional, antilipschitzWith_lineMap, AffineMap.image_vsub_image, AffineMap.deriv, lineMap_slope_slope_sub_div_sub, Affine.Simplex.affineCombination_mem_setInterior_iff, EuclideanGeometry.inversion_eq_lineMap, AffineMap.lineMap_mem_affineSpan_pair, AddTorsor.convexComboPair_eq_lineMap, dist_sq_lineMap_of_inner_eq_zero, signedDist_left_lineMap, Affine.Simplex.restrict_map_inclusion, Sbtw.mem_image_Ioo, nndist_self_homothety, AffineSubspace.coe_comap, AffineMap.lineMap_vadd, Finset.centroid_def, lineMap_lt_map_iff_slope_lt_slope_right, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Function.Injective.wOppSide_map_iff, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, left_lt_lineMap_iff_pos, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, AffineMap.coe_snd, AffineMap.vectorSpan_image_eq_submodule_map, nndist_homothety_self, Finset.affineCombination_subtype_eq_filter, AffineMap.coe_one, lineMap_strict_mono_right, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, homothety_one_half, AffineMap.homothety_eq_lineMap, AffineMap.lineMap_vadd_lineMap, convexHull_range_eq_exists_affineCombination, AffineMap.coe_prod, AffineMap.isOpenMap, AffineEquiv.congrLeftₗ_apply, lineMap_lt_lineMap_iff_of_lt, lineMap_mono_right, Affine.Simplex.map_points, dist_lineMap_lineMap, AffineMap.homothety_mul_apply, AffineMap.lineMap_vsub_lineMap, Path.eqOn_extend_segment, nndist_lineMap_left, Convex.combo_affine_apply, signedDist_vadd_vadd, AffineMap.coe_homothety, left_le_lineMap_iff_nonneg, lineMap_lt_left_iff_neg, Affine.Simplex.restrict_points_coe, AffineEquiv.ofBijective.symm_eq, AffineSubspace.mem_map_of_mem, Affine.Simplex.excenterExists_restrict, AffineMap.continuous_of_finiteDimensional, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff, AffineMap.affineIndependent_iff, MeasureTheory.Measure.addHaar_image_homothety, AffineSubspace.coe_map
«term_→ᵃ[_]_» 📖	CompOp	—

---

← Back to Index