Units

📁 Source: Mathlib/Algebra/Ring/Units.lean

Statistics

Metric	Count
Definitions instHasDistribNeg, instNeg	2
Theorems neg, neg_iff, sub_iff, isUnit_map, add_divp, add_eq_mul_one_add_div, coe_neg_one, divp_add, divp_add_divp, divp_add_divp_same, divp_sub, divp_sub_divp, divp_sub_divp_same, map_neg, map_neg_one, neg_divp, sub_divp, val_eq_neg_one, val_neg, isUnit_neg_one	20
Total	22

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neg 📖	mathematical	IsUnit	InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Units.isUnit
neg_iff 📖	mathematical	—	IsUnit InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	neg neg_neg
sub_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	neg_iff neg_sub

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_map 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	DFunLike.coe RingHom Semiring.toNonAssocSemiring instFunLike	—	IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass

Units

Definitions

Name	Category	Theorems
instHasDistribNeg 📖	CompOp	—
instNeg 📖	CompOp	101 math math: Subgroup.adjoinNegOne_eq_self_iff, ComplexShape.ε_succ, Complex.linearEquiv_det_conjLIE, HNNExtension.toSubgroup_neg_one, Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular, ComplexShape.χ_prev, ComplexShape.EulerCharSigns.χ_next, Equiv.Perm.sign_of_cycleType, Module.Ray.neg_units_smul, ComplexShape.eulerCharSignsDownNat_χ, Matrix.detp_neg_one_one, Equiv.Perm.signAux_swap, UpperHalfPlane.num_neg, inv_eq_self_iff, Int.negOnePow_eq_neg_one_iff, coe_neg_one, Int.normUnit_eq, Fin.sign_cycleRange, Equiv.Perm.sign_eq_prod_prod_Ioi, Subgroup.mem_adjoinNegOne_iff, ComplexShape.ε₁_ε₂, HNNExtension.toSubgroupEquiv_neg_one, Equiv.Perm.sign_of_cycleType_eq_replicate, GradedTensorProduct.tmul_coe_mul_coe_tmul, ComplexShape.TensorSigns.ε'_succ, ComplexShape.ε_down_ℕ, Equiv.Perm.decomposeFin.symm_sign, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, map_neg, Subgroup.negOne_mem_adjoinNegOne, Matrix.det_eq_detp_sub_detp, DirichletCharacter.Even.toUnitHom_eval_neg_one, UnitsInt.univ, Equiv.Perm.sign_eq_prod_prod_Iio, HNNExtension.NormalWord.unitsSMul_cancels_iff, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, Submodule.linearEquiv_det_reflection, HNNExtension.NormalWord.unitsSMulGroup_snd, UpperHalfPlane.σ_neg, ComplexShape.ε₂_ε₁, val_eq_neg_one, Fin.sign_cycleIcc_of_le, Int.negOnePow_one, Equiv.Perm.ofSign_disjoint, Equiv.Perm.sign_of_pow_two_eq_one, NumberField.Units.coe_neg_one, Int.negOnePow_odd, sq_eq_sq_iff_eq_or_eq_neg, Int.negOnePow_def, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, Equiv.Perm.signAux3_mul_and_swap, UpperHalfPlane.denom_neg, val_neg, Int.negOnePow_two_mul_add_one, Complex.linearEquiv_det_conjAe, Int.units_eq_one_or, IsCyclotomicExtension.Rat.Three.Units.mem, Matrix.detp_smul_adjp, neg_smul, HNNExtension.toSubgroupEquiv_neg_apply, Subgroup.HasDetPlusMinusOne.det_eq, HNNExtension.NormalWord.unitsSMul_neg, Matrix.detp_smul_add_adjp, CategoryTheory.CatCenter.app_neg_one_zpow, ComplexShape.eulerCharSignsUpNat_χ, Matrix.isAddUnit_detp_smul_mul_adjp, Matrix.detp_mul, GradedTensorProduct.comm_coe_tmul_coe, UpperHalfPlane.det_J, ComplexShape.χ_next, TensorProduct.tmul_of_gradedMul_of_tmul, HNNExtension.NormalWord.unitsSMulEquiv_symm_apply, IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq, Matrix.mul_adjp_apply_ne, Matrix.det_neg_eq_smul, sign_finRotate, Equiv.Perm.IsCycle.sign, Equiv.Perm.IsSwap.sign_eq, TensorProduct.gradedCommAux_lof_tmul, Int.units_ne_iff_eq_neg, DirichletCharacter.Odd.toUnitHom_eval_neg_one, Module.Basis.orientation_neg_single, Equiv.Perm.sign_prod_list_swap, UpperHalfPlane.neg_smul, Matrix.GLPos.coe_neg_GL, Equiv.Perm.sign_of_cycleType', CategoryTheory.CommShift₂Setup.int_ε, Equiv.Perm.ofSign_disjUnion, TensorProduct.gradedComm_of_tmul_of, Int.negOnePow_succ, Matrix.mul_adjp_add_detp, TotalComplexShape.ε₂_ε₁, Equiv.Perm.sign_swap', Equiv.Perm.sign_swap, FiniteField.prod_univ_units_id_eq_neg_one, Matrix.isAddUnit_detp_mul_detp, HNNExtension.ReducedWord.exists_normalWord_prod_eq, map_neg_one, eq_or_eq_neg_of_sq_eq_sq, CategoryTheory.CommShift₂Setup.int_z

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_divp 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul val	—	add_mul Distrib.rightDistribClass mul_inv_cancel_right
add_eq_mul_one_add_div 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Units instInv	—	mul_add Distrib.leftDistribClass mul_one mul_assoc mul_inv one_mul
coe_neg_one 📖	mathematical	—	val Units instNeg instOne InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	—
divp_add 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul val	—	add_mul Distrib.rightDistribClass mul_inv_cancel_right
divp_add_divp 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul val Units instMul	—	mul_inv_rev add_mul Distrib.rightDistribClass mul_comm mul_assoc mul_inv inv_mul mul_one
divp_add_divp_same 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	add_mul Distrib.rightDistribClass
divp_sub 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing val	—	sub_mul mul_assoc mul_inv mul_one
divp_sub_divp 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing val Units instMul	—	sub_eq_add_neg neg_divp divp_add_divp mul_neg
divp_sub_divp_same 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	sub_eq_add_neg neg_divp divp_add_divp_same
map_neg 📖	mathematical	—	DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulOneClass.toMulOne instMulOneClass MonoidHom.instFunLike map MonoidHomClass.toMonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instNeg NonUnitalNonAssocRing.toHasDistribNeg NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg RingHomClass.toAddMonoidHomClass
map_neg_one 📖	mathematical	—	DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulOneClass.toMulOne instMulOneClass MonoidHom.instFunLike map MonoidHomClass.toMonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instNeg NonUnitalNonAssocRing.toHasDistribNeg NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOne	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
neg_divp 📖	mathematical	—	InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass divp	—	neg_mul
sub_divp 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne divp MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing val	—	sub_mul mul_inv_cancel_right
val_eq_neg_one 📖	mathematical	—	val InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne Units instNeg instOne	—	coe_neg_one
val_neg 📖	mathematical	—	val Units instNeg InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_neg_one 📖	mathematical	—	IsUnit InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	IsUnit.neg isUnit_one

---

← Back to Index