Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Group/WithOne/Defs.lean

Statistics

Metric	Count
Definitions `WithOne`, `inhabited`, `instCoeTC`, `instCommMonoid`, `instInv`, `instInvOneClass`, `instMonad`, `instMonoid`, `instMul`, `instMulOneClass`, `instOne`, `instRepr`, `recOneCoe`, `unone`, `inhabited`, `instAdd`, `instAddCommMonoid`, `instAddMonoid`, `instAddZeroClass`, `instCoeTC`, `instMonad`, `instNeg`, `instNegZeroClass`, `instRepr`, `instZero`, `recZeroCoe`, `unzero`	27
Theorems `cases_on`, `coe_inj`, `coe_injective`, `coe_inv`, `coe_mul`, `coe_ne_one`, `coe_unone`, `exists`, `forall`, `instCanLift`, `instNontrivial`, `ne_one_iff_exists`, `one_ne_coe`, `recOneCoe_coe`, `recOneCoe_one`, `unone_coe`, `cases_on`, `coe_add`, `coe_inj`, `coe_injective`, `coe_ne_zero`, `coe_neg`, `coe_unzero`, `exists`, `forall`, `instCanLift`, `instNontrivial`, `ne_zero_iff_exists`, `recZeroCoe_coe`, `recZeroCoe_zero`, `unzero_coe`, `zero_ne_coe`	32
Total	59

WithOne

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`instCoeTC` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instInv` 📖	CompOp	1 math math: `coe_inv`
`instInvOneClass` 📖	CompOp	—
`instMonad` 📖	CompOp	—
`instMonoid` 📖	CompOp	1 math math: `MonCat.adjoinOne_map`
`instMul` 📖	CompOp	6 math math: `coeMulHom_apply`, `MulEquiv.withOneCongr_symm`, `MulEquiv.withOneCongr_apply`, `coe_mul`, `MulEquiv.withOneCongr_trans`, `MulEquiv.withOneCongr_refl`
`instMulOneClass` 📖	CompOp	11 math math: `lift_coe`, `lift_symm_apply`, `mapMulHom_coe`, `mapMulHom_injective`, `mapMulHom_comp`, `mapMulHom_mapMulHom`, `mapMulHom_id`, `MulEquiv.withOneCongr_apply`, `lift_one`, `mapMulHom_injective'`, `lift_unique`
`instOne` 📖	CompOp	9 math math: `map_bot`, `exists`, `map₂_bot_left`, `recOneCoe_one`, `lift_one`, `instCanLift`, `map₂_bot_right`, `map₂_eq_bot_iff`, `forall`
`instRepr` 📖	CompOp	—
`recOneCoe` 📖	CompOp	2 math math: `recOneCoe_one`, `recOneCoe_coe`
`unone` 📖	CompOp	2 math math: `coe_unone`, `unone_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cases_on` 📖	—	`WithOne` `instOne` `coe`	—	—	—
`coe_inj` 📖	mathematical	—	`coe`	—	—
`coe_injective` 📖	mathematical	—	`WithOne` `coe`	—	`Option.some_injective`
`coe_inv` 📖	mathematical	—	`coe` `WithOne` `instInv`	—	—
`coe_mul` 📖	mathematical	—	`coe` `WithOne` `instMul`	—	—
`coe_ne_one` 📖	—	—	—	—	—
`coe_unone` 📖	mathematical	—	`coe` `unone`	—	—
`exists` 📖	mathematical	—	`WithOne` `instOne` `coe`	—	—
`forall` 📖	mathematical	—	`WithOne` `instOne` `coe`	—	—
`instCanLift` 📖	mathematical	—	`CanLift` `WithOne` `coe` `instOne`	—	`ne_one_iff_exists`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithOne`	—	`Option.nontrivial`
`ne_one_iff_exists` 📖	mathematical	—	`coe`	—	—
`one_ne_coe` 📖	—	—	—	—	`coe_ne_one`
`recOneCoe_coe` 📖	mathematical	—	`recOneCoe` `coe`	—	—
`recOneCoe_one` 📖	mathematical	—	`recOneCoe` `WithOne` `instOne`	—	—
`unone_coe` 📖	mathematical	—	`unone` `coe`	—	—

WithZero

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`instAdd` 📖	CompOp	11 math math: `instExistsAddOfLE`, `AddEquiv.withZeroCongr_apply`, `AddEquiv.withZeroCongr_symm`, `instLeftDistribClass`, `AddEquiv.withZeroCongr_refl`, `instRightDistribClass`, `AddEquiv.withZeroCongr_trans`, `addLeftMono`, `coeAddHom_apply`, `instCanonicallyOrderedAdd`, `coe_add`
`instAddCommMonoid` 📖	CompOp	1 math math: `isOrderedAddMonoid`
`instAddMonoid` 📖	CompOp	1 math math: `AddMonCat.adjoinZero_map`
`instAddZeroClass` 📖	CompOp	11 math math: `mapAddHom_comp`, `mapAddHom_id`, `AddEquiv.withZeroCongr_apply`, `lift_coe`, `lift_symm_apply`, `mapAddHom_injective'`, `mapAddHom_coe`, `lift_zero`, `lift_unique`, `mapAddHom_injective`, `mapAddHom_mapAddHom`
`instCoeTC` 📖	CompOp	—
`instMonad` 📖	CompOp	—
`instNeg` 📖	CompOp	1 math math: `coe_neg`
`instNegZeroClass` 📖	CompOp	—
`instRepr` 📖	CompOp	—
`instZero` 📖	CompOp	54 math math: `instPosMulMonoWithZeroOfMulLeftMono`, `map'_zero`, `MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk`, `zero_eq_bot`, `FunctionField.InftyValuation.map_zero'`, `recZeroCoe_zero`, `Valuation.restrict_eq_zero_iff`, `Valued.extension_eq_zero_iff`, `OrderMonoidIso.withZeroUnits_symm_apply`, `IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'`, `OrderIso.withZeroUnits_symm_apply`, `Padic.mulValuation_toFun`, `instNoZeroDivisors`, `map₂_eq_bot_iff`, `pos_iff_ne_zero`, `map₂_bot_left`, `nonpos_iff_eq_zero`, `map_bot`, `MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff`, `exists`, `zero_le`, `not_lt_zero`, `Valuation.restrict_pos_iff`, `toMulBot_zero`, `lift_zero`, `IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt`, `instCanLiftMultiplicativeExpNeOfNat`, `instMulPosMonoWithZeroOfMulRightMono`, `Rat.padicValuation_eq_zero_iff`, `forall`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero`, `inv_zero`, `exp_pos`, `map₂_bot_right`, `Valuation.RankOne.zero_of_hom_zero`, `Valuation.IsEquiv.valueGroup₀Fun_zero`, `withZeroUnitsEquiv_symm_apply`, `log_zero`, `MonoidWithZeroHom.ValueGroup₀.restrict₀_apply`, `zero_lt_coe`, `MonoidWithZeroHom.ValueGroup₀.zero_or_exists_mk'`, `IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos`, `instMulPosStrictMonoWithZeroOfMulRightStrictMono`, `expRecOn_zero`, `not_coe_le_zero`, `lift'_zero`, `Valuation.RankOne.hom_eq_zero_iff`, `instPosMulStrictMonoWithZeroOfMulLeftStrictMono`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero`, `lt_def`, `toMulBot_symm_bot`, `Int.padicValuation_eq_zero_iff`, `instCanLift`
`recZeroCoe` 📖	CompOp	7 math math: `recZeroCoe_one`, `recZeroCoe_zero`, `OrderMonoidIso.withZeroUnits_apply`, `MonoidWithZeroHom.ValueGroup₀.embedding_apply`, `OrderIso.withZeroUnits_apply`, `withZeroUnitsEquiv_apply`, `recZeroCoe_coe`
`unzero` 📖	CompOp	21 math math: `unzero_mul`, `logOrderIso_apply`, `unzero_coe`, `OrderMonoidIso.withZero_symm_apply_symm_apply`, `OrderMonoidIso.withZero_symm_apply_apply`, `expOrderIso_symm_apply`, `lt_ofAdd_iff`, `WithZeroMulInt.toNNReal_neg_apply`, `coe_unzero`, `unzero_le_unzero`, `OrderMonoidIso.unitsWithZero_apply`, `unbot_le_iff`, `lt_unzero_iff`, `le_unzero_iff`, `le_ofAdd_iff`, `toAdd_unzero_lt_of_lt_ofAdd`, `toAdd_unzero_le_of_lt_ofAdd`, `MulEquiv.withZero_symm_apply_apply`, `unzero_lt_iff`, `unitsWithZeroEquiv_apply`, `MulEquiv.withZero_symm_apply_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cases_on` 📖	—	`WithZero` `instZero` `coe`	—	—	—
`coe_add` 📖	mathematical	—	`coe` `WithZero` `instAdd`	—	—
`coe_inj` 📖	mathematical	—	`coe`	—	—
`coe_injective` 📖	mathematical	—	`WithZero` `coe`	—	`Option.some_injective`
`coe_ne_zero` 📖	—	—	—	—	—
`coe_neg` 📖	mathematical	—	`coe` `WithZero` `instNeg`	—	—
`coe_unzero` 📖	mathematical	—	`coe` `unzero`	—	—
`exists` 📖	mathematical	—	`WithZero` `instZero` `coe`	—	—
`forall` 📖	mathematical	—	`WithZero` `instZero` `coe`	—	—
`instCanLift` 📖	mathematical	—	`CanLift` `WithZero` `coe` `instZero`	—	`ne_zero_iff_exists`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithZero`	—	`Option.nontrivial`
`ne_zero_iff_exists` 📖	mathematical	—	`coe`	—	—
`recZeroCoe_coe` 📖	mathematical	—	`recZeroCoe` `coe`	—	—
`recZeroCoe_zero` 📖	mathematical	—	`recZeroCoe` `WithZero` `instZero`	—	—
`unzero_coe` 📖	mathematical	—	`unzero` `coe`	—	—
`zero_ne_coe` 📖	—	—	—	—	`coe_ne_zero`

(root)

Definitions

Name	Category	Theorems
`WithOne` 📖	CompOp	29 math math: `WithOne.coeMulHom_apply`, `WithOne.map_bot`, `WithOne.exists`, `WithOne.lift_coe`, `WithOne.lift_symm_apply`, `WithOne.map₂_bot_left`, `WithOne.mapMulHom_coe`, `WithOne.mapMulHom_injective`, `WithOne.mapMulHom_comp`, `WithOne.recOneCoe_one`, `WithOne.mapMulHom_mapMulHom`, `WithOne.mapMulHom_id`, `MulEquiv.withOneCongr_symm`, `MulEquiv.withOneCongr_apply`, `WithOne.lift_one`, `MonCat.adjoinOne_obj_coe`, `WithOne.coe_mul`, `MulEquiv.withOneCongr_trans`, `WithOne.instCanLift`, `MonCat.adjoinOne_map`, `WithOne.instNontrivial`, `WithOne.mapMulHom_injective'`, `WithOne.map₂_bot_right`, `WithOne.map₂_eq_bot_iff`, `WithOne.coe_injective`, `MulEquiv.withOneCongr_refl`, `WithOne.forall`, `WithOne.lift_unique`, `WithOne.coe_inv`

---

← Back to Index