AffineEquiv

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

Statistics

Metric	Count
Definitions `AffineEquiv`, `apply`, `symm_apply`, `arrowCongr`, `arrowCongrEquiv`, `arrowCongrₗ`, `congrLeft`, `congrLeftₗ`, `constVAdd`, `constVAddHom`, `constVSub`, `equivLike`, `equivUnitsAffineMap`, `group`, `homothetyUnitsMulHom`, `instCoeAffineMap`, `instCoeOutEquiv`, `linear`, `linearHom`, `mk'`, `ofBijective`, `ofLinearEquiv`, `pointReflection`, `prodAssoc`, `prodComm`, `prodCongr`, `refl`, `toAffineMap`, `toEquiv`, `trans`, `vaddConst`, `toAffineEquiv`, `«term_≃ᵃ[_]_»`	33
Theorems `apply_eq_iff_eq`, `apply_eq_iff_eq_symm_apply`, `apply_lineMap`, `apply_symm_apply`, `arrowCongrEquiv_apply`, `arrowCongrEquiv_symm_apply`, `arrowCongr_apply`, `arrowCongr_symm_apply`, `arrowCongrₗ_apply`, `arrowCongrₗ_symm_apply`, `bijective`, `coeFn_inj`, `coeFn_injective`, `coe_coe`, `coe_constVSub`, `coe_constVSub_symm`, `coe_homothetyUnitsMulHom_apply`, `coe_homothetyUnitsMulHom_apply_symm`, `coe_homothetyUnitsMulHom_eq_homothetyHom_coe`, `coe_linear`, `coe_mk`, `coe_mk'`, `coe_mul`, `coe_one`, `coe_prodCongr`, `coe_refl`, `coe_refl_to_affineMap`, `coe_symm_toEquiv`, `coe_toAffineMap`, `coe_toEquiv`, `coe_trans`, `coe_trans_to_affineMap`, `congrLeft_apply`, `congrLeft_symm_apply`, `congrLeftₗ_apply`, `congrLeftₗ_symm_apply`, `constVAddHom_apply`, `constVAdd_add`, `constVAdd_apply`, `constVAdd_nsmul`, `constVAdd_symm`, `constVAdd_zero`, `constVAdd_zsmul`, `equivUnitsAffineMap_symm_apply_apply`, `equivUnitsAffineMap_symm_apply_invFun`, `equivUnitsAffineMap_symm_apply_symm_apply`, `equivUnitsAffineMap_symm_apply_toFun`, `ext`, `ext_iff`, `image_symm`, `injective`, `injective_pointReflection_left_of_injective_two_nsmul`, `injective_pointReflection_left_of_module`, `inv_def`, `linearHom_apply`, `linear_arrowCongr`, `linear_constVAdd`, `linear_equivUnitsAffineMap_symm_apply`, `linear_mk'`, `linear_ofBijective`, `linear_ofLinearEquiv`, `linear_prodAssoc`, `linear_prodComm`, `linear_prodCongr`, `linear_refl`, `linear_symm`, `linear_toAffineMap`, `linear_vaddConst`, `map_vadd`, `map_vadd'`, `mul_def`, `symm_eq`, `ofBijective_apply`, `ofLinearEquiv_apply`, `ofLinearEquiv_refl`, `ofLinearEquiv_trans_ofLinearEquiv`, `one_def`, `pointReflection_apply`, `pointReflection_apply_eq_equivPointReflection_apply`, `pointReflection_fixed_iff_of_injective_two_nsmul`, `pointReflection_fixed_iff_of_module`, `pointReflection_involutive`, `pointReflection_self`, `pointReflection_symm`, `preimage_symm`, `prodAssoc_apply`, `prodAssoc_symm_apply`, `prodComm_apply`, `prodComm_symm`, `prodCongr_apply`, `prodCongr_symm`, `range_eq`, `refl_apply`, `refl_trans`, `self_trans_symm`, `surjective`, `symm_apply_apply`, `symm_refl`, `symm_trans_self`, `toAffineMap_inj`, `toAffineMap_injective`, `toAffineMap_mk`, `toEquiv_inj`, `toEquiv_injective`, `toEquiv_pointReflection`, `toEquiv_refl`, `toEquiv_symm`, `trans_apply`, `trans_assoc`, `trans_refl`, `vaddConst_apply`, `vaddConst_symm_apply`, `val_equivUnitsAffineMap_apply`, `val_inv_equivUnitsAffineMap_apply`, `homothety_neg_one_apply`, `lineMap_vadd`, `lineMap_vsub`, `vadd_lineMap`, `vsub_lineMap`, `coe_toAffineEquiv`	120
Total	153

AffineEquiv

Definitions

Name	Category	Theorems
`arrowCongr` 📖	CompOp	3 math math: `linear_arrowCongr`, `arrowCongr_symm_apply`, `arrowCongr_apply`
`arrowCongrEquiv` 📖	CompOp	2 math math: `arrowCongrEquiv_symm_apply`, `arrowCongrEquiv_apply`
`arrowCongrₗ` 📖	CompOp	3 math math: `arrowCongrₗ_symm_apply`, `arrowCongrₗ_apply`, `linear_arrowCongr`
`congrLeft` 📖	CompOp	2 math math: `congrLeft_apply`, `congrLeft_symm_apply`
`congrLeftₗ` 📖	CompOp	2 math math: `congrLeftₗ_symm_apply`, `congrLeftₗ_apply`
`constVAdd` 📖	CompOp	11 math math: `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 math math: `constVAddHom_apply`
`constVSub` 📖	CompOp	2 math math: `coe_constVSub`, `coe_constVSub_symm`
`equivLike` 📖	CompOp	107 math math: `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`, `arrowCongrEquiv_symm_apply`, `coe_mul`, `continuous_of_finiteDimensional`, `prodComm_apply`, `span_eq_top_iff`, `apply_lineMap`, `prodAssoc_symm_apply`, `congrLeftₗ_symm_apply`, `sSameSide_map_iff`, `EuclideanGeometry.oangle_pointReflection_left`, `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`, `ContinuousAffineMap.fst_decompAffineEquiv`, `map_midpoint`, `coeFn_inj`, `apply_symm_apply`, `arrowCongrₗ_symm_apply`, `list_wbtw_map_iff`, `LinearEquiv.coe_toAffineEquiv`, `wSameSide_map_iff`, `congrLeft_apply`, `EuclideanGeometry.oangle_pointReflection_right`, `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`, `ContinuousAffineMap.decompAffineEquiv_symm_apply`, `pointReflection_midpoint_right`, `injective_pointReflection_left_of_module`, `prodCongr_apply`, `ext_iff`, `congrLeft_symm_apply`, `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`, `arrowCongrₗ_apply`, `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`, `arrowCongr_symm_apply`, `arrowCongrEquiv_apply`, `coe_toHomeomorphOfFiniteDimensional_symm`, `ContinuousAffineEquiv.coe_symm_toAffineEquiv`, `coe_mk`, `AffineIsometryEquiv.coe_vaddConst'`, `EuclideanGeometry.angle_pointReflection_right`, `ContinuousAffineEquiv.coe_coe`, `coe_toHomeomorphOfFiniteDimensional`, `range_eq`, `sbtw_map_iff`, `preimage_symm`, `ContinuousAffineMap.snd_decompAffineEquiv`, `pointReflection_midpoint_left`, `ContinuousAffineMap.decompAffineEquiv_symm_contLinear`, `wbtw_pointReflection`, `arrowCongr_apply`, `AffineSubspace.equivMapOfInjective_toFun`, `AffineSubspace.wOppSide_pointReflection`, `coeFn_injective`, `bijective`, `affineIndependent_iff`, `trans_apply`, `ContinuousAffineEquiv.prodAssoc_symm_apply`, `wbtw_map_iff`, `congrLeftₗ_apply`, `midpoint_pointReflection_right`, `AffineIsometryEquiv.coe_toAffineEquiv`
`equivUnitsAffineMap` 📖	CompOp	7 math math: `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 math math: `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 math math: `coe_homothetyUnitsMulHom_eq_homothetyHom_coe`, `coe_homothetyUnitsMulHom_apply_symm`, `coe_homothetyUnitsMulHom_apply`
`instCoeAffineMap` 📖	CompOp	—
`instCoeOutEquiv` 📖	CompOp	—
`linear` 📖	CompOp	23 math math: `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`, `ContinuousAffineMap.linear_decompAffineEquiv`, `coe_linear`, `linearHom_apply`, `linear_constVAdd`, `AffineSubspace.linear_equivMapOfInjective`, `linear_arrowCongr`, `linear_mk'`, `linear_prodCongr`, `linear_ofBijective`, `AffineIsometryEquiv.norm_map`, `map_vadd'`, `linear_prodComm`
`linearHom` 📖	CompOp	1 math math: `linearHom_apply`
`mk'` 📖	CompOp	2 math math: `coe_mk'`, `linear_mk'`
`ofBijective` 📖	CompOp	3 math math: `ofBijective_apply`, `linear_ofBijective`, `ofBijective.symm_eq`
`ofLinearEquiv` 📖	CompOp	4 math math: `linear_ofLinearEquiv`, `ofLinearEquiv_refl`, `ofLinearEquiv_apply`, `ofLinearEquiv_trans_ofLinearEquiv`
`pointReflection` 📖	CompOp	24 math math: `pointReflection_fixed_iff_of_injective_two_nsmul`, `AffineIsometryEquiv.pointReflection_toAffineEquiv`, `EuclideanGeometry.oangle_pointReflection_left`, `AffineMap.homothety_neg_one_apply`, `pointReflection_fixed_iff_of_module`, `pointReflection_involutive`, `toEquiv_pointReflection`, `EuclideanGeometry.oangle_pointReflection_right`, `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`, `EuclideanGeometry.angle_pointReflection_right`, `pointReflection_midpoint_left`, `wbtw_pointReflection`, `AffineSubspace.wOppSide_pointReflection`, `pointReflection_symm`, `midpoint_pointReflection_right`
`prodAssoc` 📖	CompOp	4 math math: `ContinuousAffineEquiv.prodAssoc_toAffineEquiv`, `prodAssoc_symm_apply`, `prodAssoc_apply`, `linear_prodAssoc`
`prodComm` 📖	CompOp	4 math math: `prodComm_apply`, `ContinuousAffineEquiv.prodComm_toAffineEquiv`, `prodComm_symm`, `linear_prodComm`
`prodCongr` 📖	CompOp	5 math math: `coe_prodCongr`, `prodCongr_apply`, `prodCongr_symm`, `linear_prodCongr`, `ContinuousAffineEquiv.prodCongr_toAffineEquiv`
`refl` 📖	CompOp	16 math math: `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 math math: `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 math math: `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 math math: `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 math math: `linear_vaddConst`, `AffineIsometryEquiv.vaddConst_toAffineEquiv`, `vaddConst_symm_apply`, `vaddConst_apply`, `AffineIsometryEquiv.coe_vaddConst'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`EquivLike.toEmbeddingLike`
`apply_eq_iff_eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_lineMap` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`AffineMap.apply_lineMap`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.apply_symm_apply`
`arrowCongrEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowCongrEquiv` `AffineEquiv` `equivLike` `symm`	—	—
`arrowCongrEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowCongrEquiv` `AffineEquiv` `equivLike` `symm`	—	—
`arrowCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instAddCommGroup` `AffineMap.instModule` `Ring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `AffineMap.instAddTorsor` `EquivLike.toFunLike` `equivLike` `arrowCongr` `symm`	—	`smulCommClass_self`
`arrowCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `CommRing.toRing` `AffineMap.instFunLike` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instAddCommGroup` `AffineMap.instModule` `Ring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `AffineMap.instAddTorsor` `EquivLike.toFunLike` `equivLike` `symm` `arrowCongr`	—	`smulCommClass_self`
`arrowCongrₗ_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `CommRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instFunLike` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `AffineMap.instAddCommGroup` `AffineMap.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `arrowCongrₗ` `AffineEquiv` `equivLike` `symm`	—	`RingHomInvPair.ids` `smulCommClass_self`
`arrowCongrₗ_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `CommRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instFunLike` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `AffineMap.instAddCommGroup` `AffineMap.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `arrowCongrₗ` `AffineEquiv` `equivLike`	—	`RingHomInvPair.ids` `smulCommClass_self`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Equiv.bijective`
`coeFn_inj` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`coeFn_injective` 📖	mathematical	—	`AffineEquiv` `DFunLike.coe` `EquivLike.toFunLike` `equivLike`	—	`DFunLike.coe_injective`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `toAffineMap` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`coe_constVSub` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `constVSub` `VSub.vsub` `AddTorsor.toVSub`	—	—
`coe_constVSub_symm` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `symm` `constVSub` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coe_homothetyUnitsMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `CommRing.toRing` `EquivLike.toFunLike` `equivLike` `MonoidHom` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MonoidHom.instFunLike` `homothetyUnitsMulHom` `AffineMap` `AffineMap.instFunLike` `AffineMap.homothety` `Units.val`	—	—
`coe_homothetyUnitsMulHom_apply_symm` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `CommRing.toRing` `EquivLike.toFunLike` `equivLike` `symm` `MonoidHom` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MonoidHom.instFunLike` `homothetyUnitsMulHom` `AffineMap` `AffineMap.instFunLike` `AffineMap.homothety` `Units.val` `Units.instInv`	—	—
`coe_homothetyUnitsMulHom_eq_homothetyHom_coe` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AffineEquiv` `CommRing.toRing` `AffineMap` `toAffineMap` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MonoidHom.instFunLike` `homothetyUnitsMulHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AffineMap.instMonoid` `AffineMap.homothetyHom` `Units.val`	—	—
`coe_linear` 📖	mathematical	—	`AffineMap.linear` `toAffineMap` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `linear`	—	—
`coe_mk` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike`	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids`
`coe_mk'` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike` `VSub.vsub` `AddTorsor.toVSub`	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `mk'` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids`
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `group`	—	—
`coe_prodCongr` 📖	mathematical	—	`toAffineMap` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodCongr` `AffineMap.prodMap`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `refl`	—	—
`coe_refl_to_affineMap` 📖	mathematical	—	`toAffineMap` `refl` `AffineMap.id`	—	—
`coe_symm_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquiv` `AffineEquiv` `equivLike` `symm`	—	—
`coe_toAffineMap` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `toAffineMap` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	—
`coe_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `AffineEquiv` `equivLike`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `trans`	—	—
`coe_trans_to_affineMap` 📖	mathematical	—	`toAffineMap` `trans` `AffineMap.comp`	—	—
`congrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instAddCommGroup` `AffineMap.instModule` `Ring.toSemiring` `AffineMap.instAddTorsor` `EquivLike.toFunLike` `equivLike` `congrLeft` `symm`	—	—
`congrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instAddCommGroup` `AffineMap.instModule` `Ring.toSemiring` `AffineMap.instAddTorsor` `EquivLike.toFunLike` `equivLike` `symm` `congrLeft`	—	—
`congrLeftₗ_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instFunLike` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `AffineMap.instAddCommGroup` `AffineMap.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congrLeftₗ` `AffineEquiv` `equivLike` `symm`	—	`RingHomInvPair.ids`
`congrLeftₗ_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instFunLike` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `AffineMap.instAddCommGroup` `AffineMap.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `congrLeftₗ` `AffineEquiv` `equivLike`	—	`RingHomInvPair.ids`
`constVAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `AffineEquiv` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MonoidHom.instFunLike` `constVAddHom` `constVAdd` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`constVAdd_add` 📖	mathematical	—	`constVAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `trans`	—	`ext` `AddSemigroupAction.add_vadd`
`constVAdd_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `constVAdd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`constVAdd_nsmul` 📖	mathematical	—	`constVAdd` `AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AffineEquiv` `Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group`	—	`MonoidHom.map_pow`
`constVAdd_symm` 📖	mathematical	—	`symm` `constVAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`ext`
`constVAdd_zero` 📖	mathematical	—	`constVAdd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `refl`	—	`ext` `zero_vadd`
`constVAdd_zsmul` 📖	mathematical	—	`constVAdd` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AffineEquiv` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `group`	—	`MonoidHom.map_zpow`
`equivUnitsAffineMap_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `MulEquiv` `Units` `AffineMap` `AffineMap.instMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnitsAffineMap` `AffineMap.instFunLike` `Units.val`	—	—
`equivUnitsAffineMap_symm_apply_invFun` 📖	mathematical	—	`Equiv.invFun` `toEquiv` `DFunLike.coe` `MulEquiv` `Units` `AffineMap` `AffineMap.instMonoid` `AffineEquiv` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnitsAffineMap` `AffineMap.instFunLike` `Units.val` `Units.instInv`	—	—
`equivUnitsAffineMap_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm` `MulEquiv` `Units` `AffineMap` `AffineMap.instMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnitsAffineMap` `AffineMap.instFunLike` `Units.val` `Units.instInv`	—	—
`equivUnitsAffineMap_symm_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `MulEquiv` `Units` `AffineMap` `AffineMap.instMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnitsAffineMap` `AffineMap.instFunLike` `Units.val`	—	—
`ext` 📖	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`ext`
`image_symm` 📖	mathematical	—	`Set.image` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm` `Set.preimage`	—	`Equiv.image_eq_preimage_symm`
`injective` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Equiv.injective`
`injective_pointReflection_left_of_injective_two_nsmul` 📖	mathematical	`AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Equiv.injective_pointReflection_left_of_injective_two_nsmul`
`injective_pointReflection_left_of_module` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Nat.instAtLeastTwoHAddOfNat` `injective_pointReflection_left_of_injective_two_nsmul` `IsUnit.smul_left_cancel` `isUnit_of_invertible` `two_smul` `two_nsmul`
`inv_def` 📖	mathematical	—	`AffineEquiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `group` `symm`	—	—
`linearHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `AffineEquiv` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `LinearEquiv.automorphismGroup` `MonoidHom.instFunLike` `linearHom` `linear`	—	`RingHomInvPair.ids`
`linear_arrowCongr` 📖	mathematical	—	`linear` `AffineMap` `CommRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineMap.instAddCommGroup` `AffineMap.instModule` `Ring.toSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction` `AffineMap.instAddTorsor` `arrowCongr` `arrowCongrₗ`	—	`RingHomInvPair.ids` `smulCommClass_self`
`linear_constVAdd` 📖	mathematical	—	`linear` `constVAdd` `LinearEquiv.refl` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids`
`linear_equivUnitsAffineMap_symm_apply` 📖	mathematical	—	`linear` `DFunLike.coe` `MulEquiv` `Units` `AffineMap` `AffineMap.instMonoid` `AffineEquiv` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `equivUnitsAffineMap` `LinearMap.GeneralLinearGroup` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap` `Module.End.instMonoid` `LinearEquiv.automorphismGroup` `LinearMap.GeneralLinearGroup.generalLinearEquiv` `MonoidHom` `Units.instMulOneClass` `MonoidHom.instFunLike` `Units.map` `AffineMap.linearHom`	—	—
`linear_mk'` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike` `VSub.vsub` `AddTorsor.toVSub`	`linear` `mk'` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`RingHomInvPair.ids`
`linear_ofBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	`linear` `ofBijective` `LinearEquiv.ofBijective` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `AffineMap.linear`	—	—
`linear_ofLinearEquiv` 📖	mathematical	—	`linear` `ofLinearEquiv`	—	`RingHomInvPair.ids`
`linear_prodAssoc` 📖	mathematical	—	`linear` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `Prod.instAddGroup` `AddCommGroup.toAddGroup` `prodAssoc` `LinearEquiv.prodAssoc`	—	`RingHomInvPair.ids`
`linear_prodComm` 📖	mathematical	—	`linear` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodComm` `LinearEquiv.prodComm`	—	`RingHomInvPair.ids`
`linear_prodCongr` 📖	mathematical	—	`linear` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodCongr` `LinearEquiv.prodCongr`	—	`RingHomInvPair.ids`
`linear_refl` 📖	mathematical	—	`linear` `refl` `LinearEquiv.refl` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids`
`linear_symm` 📖	mathematical	—	`linear` `symm` `LinearEquiv.symm` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids`
`linear_toAffineMap` 📖	mathematical	—	`AffineMap.linear` `toAffineMap` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `linear`	—	—
`linear_vaddConst` 📖	mathematical	—	`linear` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `vaddConst` `LinearEquiv.refl` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids`
`map_vadd` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike` `linear`	—	`map_vadd'`
`map_vadd'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike` `linear`	—	—
`mul_def` 📖	mathematical	—	`AffineEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `trans`	—	—
`ofBijective_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `ofBijective` `AffineMap` `AffineMap.instFunLike`	—	—
`ofLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `ofLinearEquiv` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike` `VSub.vsub` `AddTorsor.toVSub`	—	`RingHomInvPair.ids`
`ofLinearEquiv_refl` 📖	mathematical	—	`ofLinearEquiv` `LinearEquiv.refl` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `refl`	—	`ext` `vsub_vadd`
`ofLinearEquiv_trans_ofLinearEquiv` 📖	mathematical	—	`trans` `ofLinearEquiv` `LinearEquiv.trans` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `ext` `RingHomCompTriple.ids` `map_vadd` `vsub_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `zero_vadd`
`one_def` 📖	mathematical	—	`AffineEquiv` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `group` `refl`	—	—
`pointReflection_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `VSub.vsub` `AddTorsor.toVSub`	—	—
`pointReflection_apply_eq_equivPointReflection_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection` `Equiv.Perm` `Equiv.instEquivLike` `Equiv.pointReflection` `AddCommGroup.toAddGroup`	—	—
`pointReflection_fixed_iff_of_injective_two_nsmul` 📖	mathematical	`AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Equiv.pointReflection_fixed_iff_of_injective_two_nsmul`
`pointReflection_fixed_iff_of_module` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Nat.instAtLeastTwoHAddOfNat` `injective_pointReflection_left_of_module` `pointReflection_self`
`pointReflection_involutive` 📖	mathematical	—	`Function.Involutive` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`Equiv.pointReflection_involutive`
`pointReflection_self` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `pointReflection`	—	`vsub_vadd`
`pointReflection_symm` 📖	mathematical	—	`symm` `pointReflection`	—	`toEquiv_injective` `Equiv.pointReflection_symm`
`preimage_symm` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm` `Set.image`	—	`image_symm`
`prodAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `Prod.instAddGroup` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `prodAssoc`	—	—
`prodAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `Prod.instAddGroup` `EquivLike.toFunLike` `equivLike` `symm` `prodAssoc`	—	—
`prodComm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `prodComm`	—	—
`prodComm_symm` 📖	mathematical	—	`symm` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodComm`	—	—
`prodCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `prodCongr`	—	—
`prodCongr_symm` 📖	mathematical	—	`symm` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Prod.instAddTorsor` `AddCommGroup.toAddGroup` `prodCongr`	—	—
`range_eq` 📖	mathematical	—	`Set.range` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `Set.univ`	—	`EquivLike.range_eq_univ`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	`ext`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_refl` 📖	mathematical	—	`symm` `refl`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toAffineMap_inj` 📖	mathematical	—	`toAffineMap`	—	`toAffineMap_injective`
`toAffineMap_injective` 📖	mathematical	—	`AffineEquiv` `AffineMap` `toAffineMap`	—	`RingHomInvPair.ids`
`toAffineMap_mk` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.instEquivLike`	`toAffineMap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid`	—	`RingHomInvPair.ids`
`toEquiv_inj` 📖	mathematical	—	`toEquiv`	—	`toEquiv_injective`
`toEquiv_injective` 📖	mathematical	—	`AffineEquiv` `Equiv` `toEquiv`	—	`ext` `Equiv.ext_iff`
`toEquiv_pointReflection` 📖	mathematical	—	`toEquiv` `pointReflection` `Equiv.pointReflection` `AddCommGroup.toAddGroup`	—	—
`toEquiv_refl` 📖	mathematical	—	`toEquiv` `refl` `Equiv.refl`	—	—
`toEquiv_symm` 📖	mathematical	—	`toEquiv` `symm` `Equiv.symm`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	`ext`
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	`ext`
`vaddConst_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `vaddConst` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`vaddConst_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `equivLike` `symm` `vaddConst` `VSub.vsub` `AddTorsor.toVSub`	—	—
`val_equivUnitsAffineMap_apply` 📖	mathematical	—	`Units.val` `AffineMap` `AffineMap.instMonoid` `DFunLike.coe` `MulEquiv` `AffineEquiv` `Units` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivUnitsAffineMap` `toAffineMap`	—	—
`val_inv_equivUnitsAffineMap_apply` 📖	mathematical	—	`Units.val` `AffineMap` `AffineMap.instMonoid` `Units` `Units.instInv` `DFunLike.coe` `MulEquiv` `AffineEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `group` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `equivUnitsAffineMap` `toAffineMap` `symm`	—	—

AffineEquiv.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

AffineEquiv.ofBijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_eq` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	`AffineEquiv.toEquiv` `AffineEquiv.symm` `AffineEquiv.ofBijective` `Equiv.symm` `Equiv.ofBijective` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	—

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homothety_neg_one_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `CommRing.toRing` `instFunLike` `homothety` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AffineEquiv` `EquivLike.toFunLike` `AffineEquiv.equivLike` `AffineEquiv.pointReflection`	—	`neg_smul` `one_smul` `neg_vsub_eq_vsub_rev`
`lineMap_vadd` 📖	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`	—	`AffineEquiv.apply_lineMap`
`lineMap_vsub` 📖	mathematical	—	`VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instFunLike` `lineMap`	—	`AffineEquiv.apply_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`	—	`AffineEquiv.apply_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`	—	`AffineEquiv.apply_lineMap`

LinearEquiv

Definitions

Name	Category	Theorems
`toAffineEquiv` 📖	CompOp	2 math math: `coe_toAffineEquiv`, `LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toAffineEquiv` 📖	mathematical	—	`DFunLike.coe` `AffineEquiv` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `AffineEquiv.equivLike` `toAffineEquiv` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `instEquivLike`	—	`RingHomInvPair.ids`

(root)

Definitions

Name	Category	Theorems
`AffineEquiv` 📖	CompData	123 math math: `AffineEquiv.coe_symm_toEquiv`, `AffineIsometryEquiv.coe_mk`, `AffineEquiv.coe_toEquiv`, `AffineEquiv.sOppSide_map_iff`, `AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul`, `AffineIsometryEquiv.coe_symm_toAffineEquiv`, `AffineEquiv.coe_mk'`, `AffineEquiv.constVAdd_apply`, `AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe`, `AffineEquiv.arrowCongrEquiv_symm_apply`, `AffineEquiv.coe_mul`, `AffineEquiv.continuous_of_finiteDimensional`, `AffineEquiv.prodComm_apply`, `AffineEquiv.span_eq_top_iff`, `AffineEquiv.apply_lineMap`, `AffineEquiv.prodAssoc_symm_apply`, `AffineEquiv.congrLeftₗ_symm_apply`, `AffineEquiv.sSameSide_map_iff`, `EuclideanGeometry.oangle_pointReflection_left`, `AffineEquiv.linear_equivUnitsAffineMap_symm_apply`, `AffineMap.homothety_neg_one_apply`, `AffineEquiv.pointReflection_fixed_iff_of_module`, `ContinuousAffineEquiv.prodComm_symm_apply`, `AffineEquiv.ofBijective_apply`, `AffineEquiv.pointReflection_involutive`, `AffineEquiv.prodAssoc_apply`, `AffineEquiv.coe_homothetyUnitsMulHom_apply_symm`, `AffineEquiv.coe_constVSub`, `AffineEquiv.map_vadd`, `AffineEquiv.inv_def`, `ContinuousAffineMap.fst_decompAffineEquiv`, `AffineEquiv.map_midpoint`, `AffineEquiv.coeFn_inj`, `AffineEquiv.val_equivUnitsAffineMap_apply`, `AffineEquiv.apply_symm_apply`, `AffineEquiv.arrowCongrₗ_symm_apply`, `AffineEquiv.constVAdd_nsmul`, `AffineEquiv.constVAdd_zsmul`, `AffineEquiv.toEquiv_injective`, `AffineEquiv.list_wbtw_map_iff`, `LinearEquiv.coe_toAffineEquiv`, `AffineEquiv.mul_def`, `AffineEquiv.wSameSide_map_iff`, `AffineEquiv.congrLeft_apply`, `EuclideanGeometry.oangle_pointReflection_right`, `AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul`, `AffineEquiv.toAffineMap_injective`, `ContinuousAffineEquiv.toAffineEquiv_injective`, `AffineEquiv.equivUnitsAffineMap_symm_apply_apply`, `AffineEquiv.coe_one`, `sbtw_pointReflection_of_ne`, `AffineSubspace.topEquiv_symm_apply_coe`, `AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply`, `ContinuousAffineMap.decompAffineEquiv_symm_apply`, `AffineEquiv.linearHom_apply`, `AffineEquiv.pointReflection_midpoint_right`, `AffineEquiv.injective_pointReflection_left_of_module`, `AffineEquiv.prodCongr_apply`, `AffineEquiv.ext_iff`, `AffineEquiv.congrLeft_symm_apply`, `AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply`, `AffineEquiv.symm_apply_apply`, `AffineEquiv.coe_trans`, `AffineEquiv.ofLinearEquiv_apply`, `AffineEquiv.coe_refl`, `AffineEquiv.affineIndependent_set_of_eq_iff`, `AffineEquiv.pointReflection_apply`, `AffineEquiv.coe_constVSub_symm`, `AffineSubspace.comap_span`, `AffineEquiv.apply_eq_iff_eq_symm_apply`, `AffineEquiv.equivUnitsAffineMap_symm_apply_toFun`, `AffineEquiv.injective`, `AffineEquiv.arrowCongrₗ_apply`, `AffineSubspace.sOppSide_pointReflection`, `midpoint_eq_iff`, `AffineEquiv.refl_apply`, `AffineIsometryEquiv.toAffineEquiv_injective`, `AffineEquiv.coe_toAffineMap`, `AffineEquiv.image_symm`, `AffineSubspace.topEquiv_apply`, `AffineEquiv.coe_coe`, `AffineEquiv.coe_homothetyUnitsMulHom_apply`, `AffineEquiv.apply_eq_iff_eq`, `AffineEquiv.midpoint_pointReflection_left`, `AffineEquiv.surjective`, `AffineEquiv.pointReflection_self`, `AffineEquiv.coe_ofEq_apply`, `AffineEquiv.list_sbtw_map_iff`, `AffineEquiv.wOppSide_map_iff`, `AffineEquiv.vaddConst_symm_apply`, `AffineEquiv.vaddConst_apply`, `AffineEquiv.arrowCongr_symm_apply`, `AffineEquiv.arrowCongrEquiv_apply`, `AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm`, `ContinuousAffineEquiv.coe_symm_toAffineEquiv`, `AffineEquiv.val_inv_equivUnitsAffineMap_apply`, `AffineEquiv.coe_mk`, `AffineIsometryEquiv.coe_vaddConst'`, `EuclideanGeometry.angle_pointReflection_right`, `ContinuousAffineEquiv.coe_coe`, `AffineEquiv.coe_toHomeomorphOfFiniteDimensional`, `AffineEquiv.range_eq`, `AffineEquiv.sbtw_map_iff`, `AffineEquiv.preimage_symm`, `ContinuousAffineMap.snd_decompAffineEquiv`, `AffineEquiv.pointReflection_midpoint_left`, `ContinuousAffineMap.decompAffineEquiv_symm_contLinear`, `wbtw_pointReflection`, `AffineEquiv.arrowCongr_apply`, `AffineSubspace.equivMapOfInjective_toFun`, `AffineSubspace.wOppSide_pointReflection`, `AffineEquiv.coeFn_injective`, `AffineEquiv.bijective`, `AffineEquiv.affineIndependent_iff`, `AffineEquiv.trans_apply`, `ContinuousAffineEquiv.prodAssoc_symm_apply`, `AffineEquiv.wbtw_map_iff`, `AffineEquiv.equivUnitsAffineMap_symm_apply_invFun`, `AffineEquiv.congrLeftₗ_apply`, `AffineEquiv.midpoint_pointReflection_right`, `AffineEquiv.one_def`, `AffineIsometryEquiv.coe_toAffineEquiv`, `AffineEquiv.constVAddHom_apply`
`«term_≃ᵃ[_]_»` 📖	CompOp	—

---

← Back to Index