WithZero

📁 Source: Mathlib/Algebra/GroupWithZero/WithZero.lean

Statistics

Metric	Count
Definitions `unzero`, `withZero`, `coeMonoidHom`, `div`, `exp`, `expEquiv`, `expRecOn`, `instAddMonoidWithOne`, `instCommGroupWithZero`, `instCommMonoidWithZero`, `instCommSemigroup`, `instDivInvMonoid`, `instDivInvOneMonoid`, `instDivisionCommMonoid`, `instDivisionMonoid`, `instGroupWithZero`, `instInvolutiveInv`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instPowInt`, `instSemigroupWithZero`, `inv`, `invOneClass`, `lift'`, `logEquiv`, `map'`, `one`, `pow`, `unitsWithZeroEquiv`, `withZeroUnitsEquiv`, `«term_ᵐ⁰»`	32
Theorems `apply_one_apply_eq`, `comp_one`, `map_eq_zero_iff`, `one_apply_val_unit`, `withZero_apply_apply`, `withZero_apply_symm_apply`, `withZero_symm_apply_apply`, `withZero_symm_apply_symm_apply`, `coeMonoidHom_apply`, `coe_div`, `coe_expEquiv_apply`, `coe_inv`, `coe_mul`, `coe_one`, `coe_pow`, `coe_unitsWithZeroEquiv_eq_units_val`, `coe_zpow`, `expEquiv_symm`, `expRecOn_exp`, `expRecOn_zero`, `exp_add`, `exp_eq_one`, `exp_inj`, `exp_injective`, `exp_log`, `exp_ne_zero`, `exp_neg`, `exp_nsmul`, `exp_sub`, `exp_zero`, `exp_zsmul`, `instCanLiftMultiplicativeExpNeOfNat`, `instNoZeroDivisors`, `instNontrivialUnits`, `inv_zero`, `lift'_coe`, `lift'_surjective`, `lift'_symm_apply_apply`, `lift'_unique`, `lift'_zero`, `logEquiv_apply`, `logEquiv_symm`, `logEquiv_unitsMk0`, `log_div`, `log_exp`, `log_inv`, `log_mul`, `log_one`, `log_pow`, `log_zero`, `log_zpow`, `map'_coe`, `map'_comp`, `map'_id`, `map'_injective`, `map'_injective_iff`, `map'_map'`, `map'_surjective`, `map'_surjective_iff`, `map'_zero`, `monoidWithZeroHom_ext`, `monoidWithZeroHom_ext_iff`, `recZeroCoe_one`, `unitsWithZeroEquiv_apply`, `unitsWithZeroEquiv_symm_apply`, `unzero_mul`, `withZeroUnitsEquiv_apply`, `withZeroUnitsEquiv_symm_apply`, `withZeroUnitsEquiv_symm_apply_coe`	69
Total	101

MonoidWithZeroHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one_apply_eq` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `funLike` `one`	—	`eq_or_ne` `one_apply_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `monoidWithZeroHomClass` `one_apply_of_ne_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass`
`comp_one` 📖	mathematical	—	`comp` `MonoidWithZeroHom` `one`	—	`ext` `apply_one_apply_eq`
`map_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `funLike` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `CanLift.prf` `instCanLiftUnitsValIsUnit` `isUnit_iff_ne_zero` `one_ne_zero` `NeZero.one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `monoidWithZeroHomClass` `Units.mul_inv` `map_mul` `MonoidHomClass.toMulHomClass` `MulZeroClass.zero_mul` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`one_apply_val_unit` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `funLike` `one` `Units.val` `MonoidWithZero.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`one_apply_of_ne_zero` `Units.ne_zero`

MulEquiv

Definitions

Name	Category	Theorems
`unzero` 📖	CompOp	—
`withZero` 📖	CompOp	4 math math: `withZero_apply_symm_apply`, `withZero_apply_apply`, `withZero_symm_apply_apply`, `withZero_symm_apply_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withZero_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `Equiv` `Equiv.instEquivLike` `withZero` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom`	—	—
`withZero_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `Equiv.instEquivLike` `withZero` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom`	—	—
`withZero_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `Equiv` `WithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Equiv.instEquivLike` `Equiv.symm` `withZero` `WithZero.unzero` `WithZero.coe`	—	—
`withZero_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `instEquivLike` `symm` `Equiv` `WithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `Equiv.instEquivLike` `Equiv.symm` `withZero` `WithZero.unzero` `WithZero.coe`	—	—

WithZero

Definitions

Name	Category	Theorems
`coeMonoidHom` 📖	CompOp	3 math math: `monoidWithZeroHom_ext_iff`, `lift'_unique`, `coeMonoidHom_apply`
`div` 📖	CompOp	6 math math: `Ring.ordFrac_eq_div`, `exp_sub`, `Polynomial.valuation_of_mk`, `coe_div`, `log_div`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'`
`exp` 📖	CompOp	47 math math: `exp_add`, `exp_inj`, `FunctionField.inftyValuation.X_inv`, `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg`, `LaurentSeries.valuation_le_iff_coeff_lt_eq_zero`, `LaurentSeries.valuation_single_zpow`, `exp_lt_exp`, `exp_sub`, `IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem`, `coe_expEquiv_apply`, `IsDedekindDomain.HeightOneSpectrum.intValuation_singleton`, `Rat.padicValuation_self`, `FunctionField.inftyValuation.polynomial`, `log_le_iff_le_exp`, `IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer`, `lt_mul_exp_iff_le`, `FunctionField.inftyValuation_of_nonzero`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd`, `Padic.mulValuation_toFun`, `exp_eq_one`, `exp_le_exp`, `le_exp_of_log_le`, `LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`, `Int.padicValuation_self`, `expRecOn_exp`, `log_exp`, `le_log_iff_exp_le`, `exp_nsmul`, `lt_exp_of_log_lt`, `instCanLiftMultiplicativeExpNeOfNat`, `FunctionField.inftyValuation.X_zpow`, `lt_log_iff_exp_lt`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `FunctionField.inftyValuation.X`, `exp_pos`, `PowerSeries.intValuation_X`, `exp_zsmul`, `IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer`, `log_lt_iff_lt_exp`, `le_exp_log`, `exp_log`, `exp_zero`, `LaurentSeries.valuation_X_pow`, `exp_neg`, `Polynomial.valuation_X_eq_neg_one`, `exp_injective`
`expEquiv` 📖	CompOp	3 math math: `logEquiv_symm`, `coe_expEquiv_apply`, `expEquiv_symm`
`expRecOn` 📖	CompOp	2 math math: `expRecOn_exp`, `expRecOn_zero`
`instAddMonoidWithOne` 📖	CompOp	—
`instCommGroupWithZero` 📖	CompOp	—
`instCommMonoidWithZero` 📖	CompOp	3 math math: `isOrderedMonoid`, `mulArchimedean_iff`, `instMulArchimedean`
`instCommSemigroup` 📖	CompOp	—
`instDivInvMonoid` 📖	CompOp	—
`instDivInvOneMonoid` 📖	CompOp	—
`instDivisionCommMonoid` 📖	CompOp	—
`instDivisionMonoid` 📖	CompOp	—
`instGroupWithZero` 📖	CompOp	6 math math: `OrderMonoidIso.val_inv_unitsWithZero_symm_apply`, `OrderMonoidIso.val_unitsWithZero_symm_apply`, `unitsWithZeroEquiv_symm_apply`, `val_inv_expOrderIso_apply`, `logEquiv_unitsMk0`, `val_inv_logOrderIso_symm_apply`
`instInvolutiveInv` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	22 math math: `logOrderIso_apply`, `OrderMonoidIso.val_inv_unitsWithZero_symm_apply`, `val_expOrderIso_apply`, `logEquiv_symm`, `coe_unitsWithZeroEquiv_eq_units_val`, `coe_expEquiv_apply`, `expOrderIso_symm_apply`, `instIsCyclicUnitsWithZero`, `expEquiv_symm`, `OrderMonoidIso.val_unitsWithZero_symm_apply`, `LaurentSeries.exists_ratFunc_val_lt`, `instNontrivialUnits`, `unitsWithZeroEquiv_symm_apply`, `LaurentSeries.exists_Polynomial_intValuation_lt`, `OrderMonoidIso.unitsWithZero_apply`, `val_inv_expOrderIso_apply`, `logEquiv_apply`, `Valued.exists_pow_lt_of_le_exp_neg_one`, `val_logOrderIso_symm_apply`, `logEquiv_unitsMk0`, `val_inv_logOrderIso_symm_apply`, `unitsWithZeroEquiv_apply`
`instMulZeroClass` 📖	CompOp	48 math math: `unzero_mul`, `exp_add`, `instPosMulMonoWithZeroOfMulLeftMono`, `withZeroUnitsEquiv_symm_apply_coe`, `OrderMonoidIso.withZero_symm_apply_symm_apply`, `OrderMonoidIso.withZero_symm_apply_apply`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `ValuativeRel.nonempty_orderIso_withZeroMul_int_iff`, `MulEquiv.withZero_apply_symm_apply`, `lt_mul_exp_iff_le`, `OrderMonoidIso.withZeroUnits_symm_apply`, `OrderMonoidIso.withZeroUnits_apply`, `MulEquiv.withZero_apply_apply`, `instNoZeroDivisors`, `withZeroUnitsEquiv_symm_strictMono`, `OrderMonoidIso.withZero_apply_symm_apply`, `toMulBot_lt`, `instLeftDistribClass`, `log_mul`, `MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit`, `OrderMonoidIso.withZero_apply_apply`, `toMulBot_coe_ofAdd`, `FunctionField.InftyValuation.map_mul'`, `instMulLeftMono`, `instRightDistribClass`, `instMulLeftReflectLT`, `toMonoidWithZeroHom_withZeroUnitsEquiv`, `toMulBot_zero`, `instMulPosMonoWithZeroOfMulRightMono`, `toMulBot_coe`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero`, `Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange`, `withZeroUnitsEquiv_symm_apply`, `MulEquiv.withZero_symm_apply_apply`, `IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'`, `instMulPosStrictMonoWithZeroOfMulRightStrictMono`, `toMulBot_le`, `withZeroUnitsEquiv_apply`, `LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered`, `coe_mul`, `instPosMulStrictMonoWithZeroOfMulLeftStrictMono`, `MonoidWithZeroHom.commute_inl_inr`, `toMulBot_symm_bot`, `LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero`, `toMulBot_strictMono`, `withZeroUnitsEquiv_strictMono`, `LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered`, `MulEquiv.withZero_symm_apply_symm_apply`
`instMulZeroOneClass` 📖	CompOp	68 math math: `map'_mono`, `map'_zero`, `MonoidWithZeroHom.snd_comp_inl`, `map'_coe`, `lift'_symm_apply_apply`, `Ring.ordFrac_eq_div`, `NumberField.FinitePlace.norm_def'`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `map'_strictMono`, `Ring.ordFrac_eq_ord`, `MonoidWithZeroHom.fst_mono`, `WithZeroMulInt.toNNReal_pos`, `MulEquiv.withZero_apply_symm_apply`, `MonoidWithZeroHom.inl_strictMono`, `WithZeroMulInt.toNNReal_lt_one_iff`, `lift'_coe`, `map'_surjective`, `MulEquiv.withZero_apply_apply`, `OrderMonoidIso.withZero_apply_symm_apply`, `WithZeroMulInt.toNNReal_neg_apply`, `map'_injective`, `monoidWithZeroHom_ext_iff`, `MonoidWithZeroHom.fst_comp_inl`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `WithZeroMulInt.toNNReal_le_one_iff`, `MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit`, `OrderMonoidIso.withZero_apply_apply`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `lift'_unique`, `NumberField.FinitePlace.norm_def_int`, `MonoidWithZeroHom.inr_mono`, `MonoidWithZeroHom.snd_inr`, `MonoidWithZeroHom.snd_inl_apply_of_ne_zero`, `toMonoidWithZeroHom_withZeroUnitsEquiv`, `MonoidWithZeroHom.inl_injective`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `MonoidWithZeroHom.snd_mono`, `MonoidWithZeroHom.fst_apply_coe`, `MonoidWithZeroHom.fst_inl`, `MonoidWithZeroHom.fst_surjective`, `WithZeroMulInt.toNNReal_eq_one_iff`, `MonoidWithZeroHom.snd_comp_inr`, `lift'_surjective`, `MonoidWithZeroHom.inr_apply_unit`, `LinearOrderedCommGroupWithZero.fst_apply`, `WithZeroMulInt.toNNReal_strictMono`, `MonoidWithZeroHom.fst_inr_apply_of_ne_zero`, `NumberField.toNNReal_valued_eq_adicAbv`, `MonoidWithZeroHom.inr_strictMono`, `map'_surjective_iff`, `WithZeroMulInt.toNNReal_pos_apply`, `MonoidWithZeroHom.inl_mono`, `map'_comp`, `lift'_zero`, `MonoidWithZeroHom.snd_apply_coe`, `LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `MonoidWithZeroHom.inr_injective`, `map'_id`, `MonoidWithZeroHom.commute_inl_inr`, `MonoidWithZeroHom.fst_comp_inr`, `coeMonoidHom_apply`, `MonoidWithZeroHom.inl_apply_unit`, `MonoidWithZeroHom.snd_surjective`, `map'_injective_iff`, `map'_map'`
`instPowInt` 📖	CompOp	3 math math: `coe_zpow`, `log_zpow`, `exp_zsmul`
`instSemigroupWithZero` 📖	CompOp	—
`inv` 📖	CompOp	4 math math: `log_inv`, `coe_inv`, `inv_zero`, `exp_neg`
`invOneClass` 📖	CompOp	—
`lift'` 📖	CompOp	6 math math: `lift'_symm_apply_apply`, `lift'_coe`, `lift'_unique`, `toMonoidWithZeroHom_withZeroUnitsEquiv`, `lift'_surjective`, `lift'_zero`
`logEquiv` 📖	CompOp	4 math math: `logEquiv_symm`, `expEquiv_symm`, `logEquiv_apply`, `logEquiv_unitsMk0`
`map'` 📖	CompOp	18 math math: `map'_mono`, `map'_zero`, `map'_coe`, `map'_strictMono`, `MulEquiv.withZero_apply_symm_apply`, `map'_surjective`, `MulEquiv.withZero_apply_apply`, `OrderMonoidIso.withZero_apply_symm_apply`, `map'_injective`, `OrderMonoidIso.withZero_apply_apply`, `LinearOrderedCommGroupWithZero.fst_apply`, `map'_surjective_iff`, `map'_comp`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `map'_id`, `map'_injective_iff`, `map'_map'`
`one` 📖	CompOp	43 math math: `Padic.withValUniformEquiv_norm_le_one_iff`, `recZeroCoe_one`, `IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers`, `Int.padicValuation_lt_one_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_one`, `WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral`, `Int.padicValuation_eq_one_iff`, `LaurentSeries.val_le_one_iff_eq_coe`, `WithZeroMulInt.toNNReal_lt_one_iff`, `log_one`, `WeierstrassCurve.IsMinimal.val_Δ_maximal`, `IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd`, `Rat.valuation_le_one_iff_den`, `exp_eq_one`, `WeierstrassCurve.isGoodReduction_iff`, `coe_le_one`, `WithZeroMulInt.toNNReal_le_one_iff`, `FunctionField.InftyValuation.map_one'`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem`, `IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'`, `one_lt_coe`, `coe_lt_one`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd`, `WeierstrassCurve.isMinimal_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff`, `Set.unit_valuation_eq_one`, `one_le_coe`, `WithZeroMulInt.toNNReal_eq_one_iff`, `FunctionField.inftyValuation.C`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one`, `Padic.norm_rat_le_one_iff_padicValuation_le_one`, `Set.integer_valuation_le_one`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one`, `Int.padicValuation_le_one`, `coe_one`, `WeierstrassCurve.IsGoodReduction.goodReduction`, `IsDedekindDomain.HeightOneSpectrum.valuation_le_one`, `instWellFoundedGTWithZeroMultiplicativeIntLeOne`, `exp_zero`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem`, `Rat.padicValuation_le_one_iff`, `IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers`
`pow` 📖	CompOp	3 math math: `coe_pow`, `log_pow`, `exp_nsmul`
`unitsWithZeroEquiv` 📖	CompOp	3 math math: `coe_unitsWithZeroEquiv_eq_units_val`, `unitsWithZeroEquiv_symm_apply`, `unitsWithZeroEquiv_apply`
`withZeroUnitsEquiv` 📖	CompOp	6 math math: `withZeroUnitsEquiv_symm_apply_coe`, `withZeroUnitsEquiv_symm_strictMono`, `toMonoidWithZeroHom_withZeroUnitsEquiv`, `withZeroUnitsEquiv_symm_apply`, `withZeroUnitsEquiv_apply`, `withZeroUnitsEquiv_strictMono`
`«term_ᵐ⁰»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `WithZero` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `instMulZeroOneClass` `MonoidHom.instFunLike` `coeMonoidHom` `coe`	—	—
`coe_div` 📖	mathematical	—	`coe` `WithZero` `div`	—	—
`coe_expEquiv_apply` 📖	mathematical	—	`Units.val` `WithZero` `Multiplicative` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Multiplicative.monoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `Units` `EquivLike.toFunLike` `Equiv.instEquivLike` `expEquiv` `exp`	—	—
`coe_inv` 📖	mathematical	—	`coe` `WithZero` `inv`	—	—
`coe_mul` 📖	mathematical	—	`coe` `WithZero` `MulZeroClass.toMul` `instMulZeroClass`	—	—
`coe_one` 📖	mathematical	—	`coe` `WithZero` `one`	—	—
`coe_pow` 📖	mathematical	—	`coe` `WithZero` `pow`	—	—
`coe_unitsWithZeroEquiv_eq_units_val` 📖	mathematical	—	`coe` `DFunLike.coe` `MulEquiv` `Units` `WithZero` `MonoidWithZero.toMonoid` `instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `unitsWithZeroEquiv` `Units.val`	—	`coe_unzero`
`coe_zpow` 📖	mathematical	—	`coe` `WithZero` `instPowInt`	—	—
`expEquiv_symm` 📖	mathematical	—	`Equiv.symm` `Units` `WithZero` `Multiplicative` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Multiplicative.monoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `expEquiv` `logEquiv`	—	—
`expRecOn_exp` 📖	mathematical	—	`expRecOn` `exp`	—	—
`expRecOn_zero` 📖	mathematical	—	`expRecOn` `WithZero` `Multiplicative` `instZero`	—	—
`exp_add` 📖	mathematical	—	`exp` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `WithZero` `Multiplicative` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul`	—	—
`exp_eq_one` 📖	mathematical	—	`exp` `WithZero` `Multiplicative` `one` `instOneMultiplicativeOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`exp_zero`
`exp_inj` 📖	mathematical	—	`exp`	—	`exp_injective`
`exp_injective` 📖	mathematical	—	`WithZero` `Multiplicative` `exp`	—	`Equiv.injective` `coe_injective`
`exp_log` 📖	mathematical	—	`exp` `log`	—	`CanLift.prf` `instCanLift`
`exp_ne_zero` 📖	—	—	—	—	—
`exp_neg` 📖	mathematical	—	`exp` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `WithZero` `Multiplicative` `inv` `Multiplicative.inv`	—	—
`exp_nsmul` 📖	mathematical	—	`exp` `AddMonoid.toNatSMul` `WithZero` `Multiplicative` `pow` `instOneMultiplicativeOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Monoid.toNatPow` `Multiplicative.monoid`	—	—
`exp_sub` 📖	mathematical	—	`exp` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `WithZero` `Multiplicative` `div` `Multiplicative.div`	—	—
`exp_zero` 📖	mathematical	—	`exp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `WithZero` `Multiplicative` `one` `instOneMultiplicativeOfZero`	—	—
`exp_zsmul` 📖	mathematical	—	`exp` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `WithZero` `Multiplicative` `instPowInt` `instOneMultiplicativeOfZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DivInvMonoid.toZPow` `Multiplicative.divInvMonoid`	—	—
`instCanLiftMultiplicativeExpNeOfNat` 📖	mathematical	—	`CanLift` `WithZero` `Multiplicative` `exp` `instZero`	—	—
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `WithZero` `MulZeroClass.toMul` `instMulZeroClass` `instZero`	—	`Option.map₂_eq_none_iff`
`instNontrivialUnits` 📖	mathematical	—	`Nontrivial` `Units` `WithZero` `MonoidWithZero.toMonoid` `instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Function.Surjective.nontrivial` `Equiv.surjective`
`inv_zero` 📖	mathematical	—	`WithZero` `inv` `instZero`	—	—
`lift'_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift'` `coe` `MonoidHom.instFunLike`	—	—
`lift'_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidHom.instFunLike`	`WithZero` `MonoidWithZeroHom` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift'`	—	—
`lift'_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidHom.instFunLike` `Equiv` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift'` `MonoidWithZeroHom.funLike` `coe`	—	—
`lift'_unique` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift'` `MonoidHom.comp` `MonoidWithZeroHom.toMonoidHom` `coeMonoidHom`	—	`Equiv.apply_symm_apply`
`lift'_zero` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift'` `instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	—
`logEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Units` `WithZero` `Multiplicative` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Multiplicative.monoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `logEquiv` `log` `Units.val`	—	—
`logEquiv_symm` 📖	mathematical	—	`Equiv.symm` `Units` `WithZero` `Multiplicative` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Multiplicative.monoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `logEquiv` `expEquiv`	—	—
`logEquiv_unitsMk0` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Units` `WithZero` `Multiplicative` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Multiplicative.monoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `logEquiv` `instGroupWithZero` `Multiplicative.group` `log`	—	`logEquiv_apply`
`log_div` 📖	mathematical	—	`log` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `WithZero` `Multiplicative` `div` `Multiplicative.div` `SubNegMonoid.toSub`	—	`CanLift.prf` `instCanLift`
`log_exp` 📖	mathematical	—	`log` `exp`	—	—
`log_inv` 📖	mathematical	—	`log` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `WithZero` `Multiplicative` `inv` `Multiplicative.inv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`inv_zero` `neg_zero`
`log_mul` 📖	mathematical	—	`log` `WithZero` `Multiplicative` `MulZeroClass.toMul` `instMulZeroClass` `Multiplicative.mul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`CanLift.prf` `instCanLift`
`log_one` 📖	mathematical	—	`log` `WithZero` `Multiplicative` `one` `instOneMultiplicativeOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`log_pow` 📖	mathematical	—	`log` `WithZero` `Multiplicative` `pow` `instOneMultiplicativeOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Monoid.toNatPow` `Multiplicative.monoid` `AddMonoid.toNatSMul`	—	`pow_zero` `nsmul_zero` `zero_pow`
`log_zero` 📖	mathematical	—	`log` `WithZero` `Multiplicative` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`log_zpow` 📖	mathematical	—	`log` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `WithZero` `Multiplicative` `instPowInt` `instOneMultiplicativeOfZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DivInvMonoid.toZPow` `Multiplicative.divInvMonoid` `SubNegMonoid.toZSMul`	—	`zpow_natCast` `log_pow` `natCast_zsmul` `zpow_negSucc` `log_inv` `negSucc_zsmul`
`map'_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'` `coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	—	—
`map'_comp` 📖	mathematical	—	`map'` `MonoidHom.comp` `MulOneClass.toMulOne` `MonoidWithZeroHom.comp` `WithZero` `instMulZeroOneClass`	—	`MonoidWithZeroHom.ext` `map'_map'`
`map'_id` 📖	mathematical	—	`MonoidHomClass.toMonoidHom` `WithZero` `MonoidWithZeroHom` `instMulZeroOneClass` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZeroHom.funLike` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `map'` `MonoidHom.id`	—	`MonoidHom.ext` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`map'_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`WithZero` `MonoidWithZeroHom` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'`	—	`map'_injective_iff`
`map'_injective_iff` 📖	mathematical	—	`WithZero` `DFunLike.coe` `MonoidWithZeroHom` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`map'_map'` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'` `MonoidHom.comp` `MulOneClass.toMulOne`	—	—
`map'_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`WithZero` `MonoidWithZeroHom` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'`	—	`map'_surjective_iff`
`map'_surjective_iff` 📖	mathematical	—	`WithZero` `DFunLike.coe` `MonoidWithZeroHom` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`map'_zero` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `instMulZeroOneClass` `MonoidWithZeroHom.funLike` `map'` `instZero`	—	—
`monoidWithZeroHom_ext` 📖	—	`MonoidHom.comp` `WithZero` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `instMulZeroOneClass` `MonoidWithZeroHom.toMonoidHom` `coeMonoidHom`	—	—	`DFunLike.ext` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `DFunLike.congr_fun`
`monoidWithZeroHom_ext_iff` 📖	mathematical	—	`MonoidHom.comp` `WithZero` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `instMulZeroOneClass` `MonoidWithZeroHom.toMonoidHom` `coeMonoidHom`	—	`monoidWithZeroHom_ext`
`recZeroCoe_one` 📖	mathematical	—	`recZeroCoe` `WithZero` `one`	—	—
`unitsWithZeroEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Units` `WithZero` `MonoidWithZero.toMonoid` `instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `unitsWithZeroEquiv` `unzero` `Units.val`	—	—
`unitsWithZeroEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Units` `WithZero` `MonoidWithZero.toMonoid` `instMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `unitsWithZeroEquiv` `instGroupWithZero` `coe` `coe_ne_zero`	—	—
`unzero_mul` 📖	mathematical	—	`unzero` `WithZero` `MulZeroClass.toMul` `instMulZeroClass` `left_ne_zero_of_mul` `right_ne_zero_of_mul`	—	`left_ne_zero_of_mul` `right_ne_zero_of_mul` `coe_unzero`
`withZeroUnitsEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulZeroClass.toMul` `instMulZeroClass` `Units.instMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `withZeroUnitsEquiv` `recZeroCoe` `MulZeroClass.toZero` `Units.val`	—	—
`withZeroUnitsEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `instMulZeroClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `withZeroUnitsEquiv` `MulZeroClass.toZero` `instZero` `coe`	—	—
`withZeroUnitsEquiv_symm_apply_coe` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `instMulZeroClass` `Units.instMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `withZeroUnitsEquiv` `Units.val` `coe`	—	`GroupWithZero.toNontrivial`

---

← Back to Index