WithAbs

📁 Source: Mathlib/Analysis/Normed/Ring/WithAbs.lean

Statistics

Metric	Count
Definitions `LiesOver`, `algEquiv`, `algebraLeft`, `delabToAbs`, `equiv`, `equivWithAbs`, `instAlgebra`, `instAlgebra_left`, `instAlgebra_right`, `instCommRing`, `instCommSemiring`, `instInhabited`, `instModule`, `instModule_left`, `instModule_right`, `instRing`, `instSMul`, `instSMul_1`, `instSemiring`, `instUnique`, `linearEquiv`, `map`, `moduleLeft`, `normedRing`, `ofAbs`	25
Theorems `comp_eq`, `algEquiv_apply`, `algEquiv_symm_apply`, `algebraMap_left_apply`, `algebraMap_left_injective`, `algebraMap_right_apply`, `algebraMap_right_injective`, `congr_apply`, `congr_refl`, `congr_symm`, `congr_symm_apply`, `congr_trans`, `equivWithAbs_equiv_symm_apply`, `equivWithAbs_symm`, `equivWithAbs_symm_equiv_symm_apply`, `equiv_apply`, `equiv_equivWithAbs_symm_apply`, `equiv_symm_apply`, `instFaithfulSMul`, `instFaithfulSMul_1`, `instIsScalarTower`, `instIsScalarTower_1`, `instIsScalarTower_2`, `instNontrivial`, `linearEquiv_apply`, `linearEquiv_symm_apply`, `map_apply`, `map_comp`, `map_id`, `norm_eq_abv`, `norm_eq_abv'`, `norm_eq_apply_ofAbs`, `norm_toAbs_eq`, `ofAbs_add`, `ofAbs_algebraMap`, `ofAbs_bijective`, `ofAbs_eq_zero`, `ofAbs_injective`, `ofAbs_mul`, `ofAbs_neg`, `ofAbs_one`, `ofAbs_pow`, `ofAbs_sub`, `ofAbs_surjective`, `ofAbs_toAbs`, `ofAbs_zero`, `smul_left_def`, `smul_right_def`, `toAbs_add`, `toAbs_bijective`, `toAbs_eq_zero`, `toAbs_injective`, `toAbs_mul`, `toAbs_neg`, `toAbs_ofAbs`, `toAbs_one`, `toAbs_pow`, `toAbs_sub`, `toAbs_surjective`, `toAbs_zero`	60
Total	85

AbsoluteValue

Definitions

Name	Category	Theorems
`LiesOver` 📖	CompData	1 math math: `NumberField.InfinitePlace.LiesOver.instLiesOverRealValAbsoluteValueExistsRingHomComplexEqPlaceMkOfLiesOver`

AbsoluteValue.LiesOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	—	`AbsoluteValue.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHom.injective` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Semiring.toNonAssocSemiring`	—	—

WithAbs

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	2 math math: `algEquiv_symm_apply`, `algEquiv_apply`
`algebraLeft` 📖	CompOp	6 math math: `algebraMap_left_apply`, `algebraMap_left_injective`, `ofAbs_algebraMap`, `NumberField.InfinitePlace.Completion.algebraMap_coe`, `instIsSeparable`, `NumberField.InfinitePlace.LiesOver.isometry_algebraMap`
`delabToAbs` 📖	CompOp	—
`equiv` 📖	CompOp	13 math math: `NumberField.InfinitePlace.isometry_embedding`, `NumberField.InfinitePlace.Completion.norm_coe`, `tendsto_one_div_one_add_pow_nhds_one`, `NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe`, `NumberField.InfinitePlace.Completion.extensionEmbedding_coe`, `equivWithAbs_equiv_symm_apply`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `equiv_equivWithAbs_symm_apply`, `equiv_apply`, `NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv`, `equiv_symm_apply`, `AbsoluteValue.Completion.extensionEmbedding_of_comp_coe`, `equivWithAbs_symm_equiv_symm_apply`
`equivWithAbs` 📖	CompOp	—
`instAlgebra` 📖	CompOp	9 math math: `algEquiv_symm_apply`, `algebraMap_right_apply`, `instIsSeparable_1`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`, `ofAbs_algebraMap`, `algEquiv_apply`, `NumberField.InfinitePlace.Completion.algebraMap_coe`, `algebraMap_right_injective`, `NumberField.InfinitePlace.LiesOver.isometry_algebraMap`
`instAlgebra_left` 📖	CompOp	—
`instAlgebra_right` 📖	CompOp	—
`instCommRing` 📖	CompOp	1 math math: `instIsSeparable`
`instCommSemiring` 📖	CompOp	5 math math: `algebraMap_left_apply`, `algebraMap_left_injective`, `ofAbs_algebraMap`, `NumberField.InfinitePlace.Completion.algebraMap_coe`, `NumberField.InfinitePlace.LiesOver.isometry_algebraMap`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	3 math math: `linearEquiv_symm_apply`, `linearEquiv_apply`, `instFiniteDimensional_1`
`instModule_left` 📖	CompOp	—
`instModule_right` 📖	CompOp	—
`instRing` 📖	CompOp	11 math math: `ofAbs_neg`, `toAbs_sub`, `ofAbs_sub`, `tendsto_one_div_one_add_pow_nhds_one`, `instIsSeparable_1`, `AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `instFiniteDimensional_1`, `AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp`, `AbsoluteValue.Completion.extensionEmbedding_of_comp_coe`, `toAbs_neg`
`instSMul` 📖	CompOp	4 math math: `instIsScalarTower_2`, `smul_left_def`, `instIsScalarTower`, `instFaithfulSMul`
`instSMul_1` 📖	CompOp	5 math math: `instIsScalarTower_2`, `instUniformContinuousConstSMulReal`, `instFaithfulSMul_1`, `instIsScalarTower_1`, `smul_right_def`
`instSemiring` 📖	CompOp	54 math math: `AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs`, `congr_refl`, `NumberField.InfinitePlace.isometry_embedding`, `ofAbs_add`, `NumberField.InfinitePlace.Completion.norm_coe`, `algEquiv_symm_apply`, `map_id`, `isometry_of_comp`, `uniformSpace_comap_eq_of_comp`, `congr_symm_apply`, `tendsto_one_div_one_add_pow_nhds_one`, `algebraMap_right_apply`, `toAbs_add`, `NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe`, `toAbs_one`, `toAbs_pow`, `toAbs_eq_zero`, `AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero`, `ofAbs_one`, `ofAbs_mul`, `ofAbs_zero`, `NumberField.InfinitePlace.Completion.extensionEmbedding_coe`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`, `ofAbs_pow`, `congr_apply`, `equivWithAbs_equiv_symm_apply`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `equiv_equivWithAbs_symm_apply`, `AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp`, `ofAbs_algebraMap`, `linearEquiv_symm_apply`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `algEquiv_apply`, `map_apply`, `NumberField.InfinitePlace.Completion.algebraMap_coe`, `map_comp`, `congr_trans`, `isUniformInducing_of_comp`, `congr_symm`, `equivWithAbs_symm`, `pseudoMetricSpace_induced_of_comp`, `equiv_apply`, `linearEquiv_apply`, `toAbs_mul`, `toAbs_zero`, `NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv`, `ofAbs_eq_zero`, `algebraMap_right_injective`, `NumberField.InfinitePlace.LiesOver.isometry_algebraMap`, `AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp`, `equiv_symm_apply`, `AbsoluteValue.isEquiv_iff_isHomeomorph`, `AbsoluteValue.Completion.extensionEmbedding_of_comp_coe`, `equivWithAbs_symm_equiv_symm_apply`
`instUnique` 📖	CompOp	—
`linearEquiv` 📖	CompOp	2 math math: `linearEquiv_symm_apply`, `linearEquiv_apply`
`map` 📖	CompOp	3 math math: `map_id`, `map_apply`, `map_comp`
`moduleLeft` 📖	CompOp	1 math math: `instFiniteDimensional`
`normedRing` 📖	CompOp	4 math math: `norm_eq_abv`, `norm_toAbs_eq`, `norm_eq_apply_ofAbs`, `norm_eq_abv'`
`ofAbs` 📖	CompOp	27 math math: `algebraMap_left_apply`, `ofAbs_surjective`, `ofAbs_add`, `toAbs_ofAbs`, `ofAbs_neg`, `ofAbs_toAbs`, `ofAbs_div`, `ofAbs_sub`, `congr_symm_apply`, `smul_left_def`, `ofAbs_one`, `ofAbs_mul`, `ofAbs_zero`, `norm_eq_abv`, `ofAbs_pow`, `congr_apply`, `ofAbs_algebraMap`, `algEquiv_apply`, `map_apply`, `norm_eq_apply_ofAbs`, `equiv_apply`, `ofAbs_injective`, `linearEquiv_apply`, `ofAbs_inv`, `ofAbs_eq_zero`, `ofAbs_bijective`, `smul_right_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `WithAbs` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `algEquiv` `ofAbs`	—	—
`algEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `WithAbs` `instSemiring` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquiv` `toAbs`	—	—
`algebraMap_left_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WithAbs` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `algebraLeft` `ofAbs`	—	—
`algebraMap_left_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`WithAbs` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `algebraLeft`	—	`ofAbs_injective`
`algebraMap_right_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WithAbs` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `toAbs`	—	—
`algebraMap_right_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`WithAbs` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra`	—	`toAbs_injective`
`congr_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congr` `toAbs` `ofAbs`	—	—
`congr_refl` 📖	mathematical	—	`congr` `RingEquiv.refl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `WithAbs` `instSemiring`	—	—
`congr_symm` 📖	mathematical	—	`RingEquiv.symm` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `congr`	—	—
`congr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `congr` `toAbs` `ofAbs`	—	—
`congr_trans` 📖	mathematical	—	`congr` `RingEquiv.trans` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `WithAbs` `instSemiring`	—	—
`equivWithAbs_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congr` `RingEquiv.refl` `RingEquiv.symm` `equiv`	—	—
`equivWithAbs_symm` 📖	mathematical	—	`RingEquiv.symm` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `congr` `RingEquiv.refl`	—	`congr_symm`
`equivWithAbs_symm_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `congr` `RingEquiv.refl` `equiv`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `ofAbs`	—	—
`equiv_equivWithAbs_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `RingEquiv.symm` `congr` `RingEquiv.refl`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equiv` `toAbs`	—	—
`instFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `WithAbs` `instSMul`	—	`ofAbs_injective` `FaithfulSMul.eq_of_smul_eq_smul`
`instFaithfulSMul_1` 📖	mathematical	—	`FaithfulSMul` `WithAbs` `instSMul_1`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `WithAbs` `instSMul`	—	`smul_assoc`
`instIsScalarTower_1` 📖	mathematical	—	`IsScalarTower` `WithAbs` `instSMul_1`	—	`Equiv.isScalarTower`
`instIsScalarTower_2` 📖	mathematical	—	`IsScalarTower` `WithAbs` `instSMul_1` `instSMul`	—	`smul_assoc`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithAbs`	—	`Equiv.nontrivial`
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithAbs` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `ofAbs`	—	`RingHomInvPair.ids`
`linearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithAbs` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv` `toAbs`	—	`RingHomInvPair.ids`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WithAbs` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map` `toAbs` `ofAbs`	—	—
`map_comp` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—
`norm_eq_abv` 📖	mathematical	—	`Norm.norm` `WithAbs` `Real` `Real.semiring` `Real.partialOrder` `Ring.toSemiring` `NormedRing.toNorm` `normedRing` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `ofAbs`	—	`norm_eq_apply_ofAbs`
`norm_eq_abv'` 📖	mathematical	—	`Norm.norm` `WithAbs` `Real` `Real.semiring` `Real.partialOrder` `Ring.toSemiring` `NormedRing.toNorm` `normedRing` `toAbs` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	`norm_toAbs_eq`
`norm_eq_apply_ofAbs` 📖	mathematical	—	`Norm.norm` `WithAbs` `Real` `Real.semiring` `Real.partialOrder` `Ring.toSemiring` `NormedRing.toNorm` `normedRing` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `ofAbs`	—	—
`norm_toAbs_eq` 📖	mathematical	—	`Norm.norm` `WithAbs` `Real` `Real.semiring` `Real.partialOrder` `Ring.toSemiring` `NormedRing.toNorm` `normedRing` `toAbs` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike`	—	—
`ofAbs_add` 📖	mathematical	—	`ofAbs` `WithAbs` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	—
`ofAbs_algebraMap` 📖	mathematical	—	`ofAbs` `DFunLike.coe` `RingHom` `WithAbs` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `instCommSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `algebraLeft` `instAlgebra`	—	—
`ofAbs_bijective` 📖	mathematical	—	`Function.Bijective` `WithAbs` `ofAbs`	—	`ofAbs_injective` `ofAbs_surjective`
`ofAbs_eq_zero` 📖	mathematical	—	`ofAbs` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	`ofAbs_injective`
`ofAbs_injective` 📖	mathematical	—	`WithAbs` `ofAbs`	—	`toAbs_ofAbs`
`ofAbs_mul` 📖	mathematical	—	`ofAbs` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	—
`ofAbs_neg` 📖	mathematical	—	`ofAbs` `Ring.toSemiring` `WithAbs` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instRing`	—	—
`ofAbs_one` 📖	mathematical	—	`ofAbs` `WithAbs` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiring`	—	—
`ofAbs_pow` 📖	mathematical	—	`ofAbs` `WithAbs` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	—
`ofAbs_sub` 📖	mathematical	—	`ofAbs` `Ring.toSemiring` `WithAbs` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instRing`	—	—
`ofAbs_surjective` 📖	mathematical	—	`WithAbs` `ofAbs`	—	`ofAbs_toAbs`
`ofAbs_toAbs` 📖	mathematical	—	`ofAbs` `toAbs`	—	—
`ofAbs_zero` 📖	mathematical	—	`ofAbs` `WithAbs` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	—
`smul_left_def` 📖	mathematical	—	`WithAbs` `instSMul` `ofAbs`	—	—
`smul_right_def` 📖	mathematical	—	`WithAbs` `instSMul_1` `toAbs` `ofAbs`	—	—
`toAbs_add` 📖	mathematical	—	`toAbs` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—
`toAbs_bijective` 📖	mathematical	—	`Function.Bijective` `WithAbs` `toAbs`	—	`toAbs_injective` `toAbs_surjective`
`toAbs_eq_zero` 📖	mathematical	—	`toAbs` `WithAbs` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`toAbs_injective`
`toAbs_injective` 📖	mathematical	—	`WithAbs` `toAbs`	—	`ofAbs_toAbs`
`toAbs_mul` 📖	mathematical	—	`toAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—
`toAbs_neg` 📖	mathematical	—	`toAbs` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `WithAbs` `instRing`	—	—
`toAbs_ofAbs` 📖	mathematical	—	`toAbs` `ofAbs`	—	—
`toAbs_one` 📖	mathematical	—	`toAbs` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—
`toAbs_pow` 📖	mathematical	—	`toAbs` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `WithAbs` `instSemiring`	—	—
`toAbs_sub` 📖	mathematical	—	`toAbs` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `WithAbs` `instRing`	—	—
`toAbs_surjective` 📖	mathematical	—	`WithAbs` `toAbs`	—	`toAbs_ofAbs`
`toAbs_zero` 📖	mathematical	—	`toAbs` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `WithAbs` `instSemiring`	—	—

---

← Back to Index