Units

📁 Source: Mathlib/Algebra/Group/Action/Units.lean

Statistics

Metric	Count
Definitions addAction', instAddAction, instVAdd, instMulAction, instSMul, mulAction', mulDistribMulActionRight	7
Theorems instFaithfulVAdd, instVAddAssocClass, vaddAssocClass', vaddAssocClass'_left, vaddCommClass', vaddCommClass_left, vaddCommClass_right, vadd_def, vadd_mk_apply, vadd_neg, val_vadd, neg_vadd, vadd, inv_smul, smul, coe_inv_smul, coe_smul, instFaithfulSMul, instIsScalarTower, isScalarTower', isScalarTower'_left, smulCommClass', smulCommClass_left, smulCommClass_right, smul_def, smul_eq_mul, smul_inv, smul_isUnit, smul_mk_apply, val_smul	30
Total	37

AddUnits

Definitions

Name	Category	Theorems
addAction' 📖	CompOp	5 math math: vaddAssocClass', val_vadd, vaddAssocClass'_left, vadd_neg, vaddCommClass'
instAddAction 📖	CompOp	—
instVAdd 📖	CompOp	13 math math: vadd_def, instFaithfulVAdd, vaddCommClass_left, isIsometricVAdd, vaddAssocClass'_left, measurableVAdd, continuousVAdd, vaddCommClass_right, instVAddAssocClass, IsAddUnit.neg_vadd, continuousConstVAdd, instMeasurableConstVAdd, vadd_mk_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulVAdd 📖	mathematical	—	FaithfulVAdd AddUnits instVAdd	—	ext FaithfulVAdd.eq_of_vadd_eq_vadd
instVAddAssocClass 📖	mathematical	—	VAddAssocClass AddUnits instVAdd	—	vadd_assoc
vaddAssocClass' 📖	mathematical	—	VAddAssocClass AddUnits AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction addAction'	—	ext vadd_assoc
vaddAssocClass'_left 📖	mathematical	—	VAddAssocClass AddUnits AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction addAction' instVAdd	—	vadd_assoc
vaddCommClass' 📖	mathematical	—	VAddCommClass AddUnits AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction addAction'	—	ext VAddCommClass.vadd_comm
vaddCommClass_left 📖	mathematical	—	VAddCommClass AddUnits instVAdd	—	VAddCommClass.vadd_comm
vaddCommClass_right 📖	mathematical	—	VAddCommClass AddUnits instVAdd	—	VAddCommClass.vadd_comm
vadd_def 📖	mathematical	—	HVAdd.hVAdd AddUnits instHVAdd instVAdd val	—	—
vadd_mk_apply 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddZero.toZero	HVAdd.hVAdd AddUnits instHVAdd instVAdd	—	—
vadd_neg 📖	mathematical	—	AddUnits instNeg HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction addAction' NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	ext
val_vadd 📖	mathematical	—	val HVAdd.hVAdd AddUnits instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction addAction'	—	—

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neg_vadd 📖	mathematical	IsAddUnit	HVAdd.hVAdd AddUnits instHVAdd AddUnits.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction AddUnits.instNeg addUnit AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	val_neg_add
vadd 📖	mathematical	IsAddUnit	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	AddUnits.val_vadd

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_smul 📖	mathematical	IsUnit	Units Units.instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction Units.instInv unit MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	val_inv_mul
smul 📖	mathematical	IsUnit	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Units.val_smul

Units

Definitions

Name	Category	Theorems
instMulAction 📖	CompOp	33 math math: WeierstrassCurve.Projective.nonsingularLift_some, WeierstrassCurve.Projective.Point.zero_point, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.Point.fromAffine_some, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.nonsingularLift_iff, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, WeierstrassCurve.Jacobian.nonsingularLift_some, WeierstrassCurve.Projective.addMap_eq, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right, WeierstrassCurve.Projective.Point.fromAffine_some, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingularLift_iff, Module.stabilizer_units_eq_bot_of_ne_zero, WeierstrassCurve.Jacobian.nonsingularLift_zero, WeierstrassCurve.Projective.addMap_of_Y_eq, WeierstrassCurve.Projective.negMap_eq, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right, WeierstrassCurve.Projective.Point.zero_def, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.Point.zero_point, WeierstrassCurve.Jacobian.Point.zero_def, orbitRel_nonZero_iff, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, WeierstrassCurve.Jacobian.negMap_eq, smul_eq_mul, WeierstrassCurve.Jacobian.addMap_of_Y_eq, WeierstrassCurve.Projective.nonsingularLift_zero
instSMul 📖	CompOp	172 math math: CochainComplex.HomComplex.δ_units_smul, AlternatingMap.domCoprod.summand_mk'', Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, Matrix.det_apply, CochainComplex.HomComplex.Cochain.δ_single, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul', ContinuousMultilinearMap.alternatization_apply_apply, AlternatingMap.map_perm, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁, spectrum.units_smul_resolvent_self, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, smul_coe, Module.Basis.repr_isUnitSMul, HomologicalComplex.mapBifunctor₂₃.d₂_eq, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj, HomologicalComplex₂.totalAux.d₂_eq, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, CochainComplex.HomComplex.Cocycle.coe_units_smul, CochainComplex.HomComplex.Cochain.units_smul_comp, autAdjoinRootXPowSubCEquiv_symm_smul, HomologicalComplex.mapBifunctor₂₃.d₃_eq, quasispectrum.mem_iff_of_isUnit, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, Polynomial.monic_of_isUnit_leadingCoeff_inv_smul, CochainComplex.HomComplex.δ_v, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, smulCommClass_left, CategoryTheory.Linear.units_smul_comp, instStarModule, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, smul_mk0, isIsometricSMul, IsUnit.inv_smul, GradedTensorProduct.tmul_coe_mul_coe_tmul, Matrix.inv_smul', CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, Ring.choose_neg, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CochainComplex.HomComplex.Cochain.leftShift_comp, CategoryTheory.Preadditive.smul_iso_hom, instIsScalarTower, AlternatingMap.map_congr_perm, spectrum.smul_mem_smul_iff, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, HomologicalComplex₂.d₁_eq, CochainComplex.HomComplex.Cochain.leftShift_rightShift, CategoryTheory.Preadditive.smul_iso_inv, MultilinearMap.domCoprod_alternization_coe, smul_isUnit, LinearMap.CompatibleSMul.units, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, HomologicalComplex.units_smul_f_apply, CochainComplex.HomComplex.Cochain.leftUnshift_v, Submodule.IsLattice.smul, CochainComplex.HomComplex.Cochain.rightShift_leftShift, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex₂.totalAux.d₁_eq, smul_mk_apply, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex.mapBifunctor.d₂_eq, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, Matrix.inv_adjugate, CategoryTheory.Linear.comp_units_smul, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, Projectivization.mk_eq_mk_iff, CochainComplex.HomComplex.δ_comp, measurableSMul, instMeasurableConstSMul, smulCommClass_right, Ring.choose_neg', AbsoluteValue.map_units_int_smul, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, CochainComplex.shiftFunctor_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, Projectivization.exists_smul_eq_mk_rep, HomologicalComplex.mapBifunctor₂₃.d₁_eq, CochainComplex.HomComplex.Cochain.shift_units_smul, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det', nnnorm_units_zsmul, MultilinearMap.alternatization_apply, CochainComplex.HomComplex.Cochain.units_smul_v, CochainComplex.HomComplex.Cochain.δ_toSingleMk, IsCompactOperator.smul_unit_iff, continuousConstSMul, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, neg_smul, CategoryTheory.Functor.map_units_smul, CochainComplex.HomComplex.Cochain.rightShift_units_smul, mem_skewAdjointMatricesLieSubalgebra_unit_smul, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, smul_def, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, CochainComplex.HomComplex.Cochain.comp_units_smul, HomologicalComplex₂.d₂_eq, CategoryTheory.CatCenter.app_neg_one_zpow, CochainComplex.HomComplex.Cochain.δ_rightUnshift, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, GradedTensorProduct.comm_coe_tmul_coe, CochainComplex.HomComplex.Cochain.δ_rightShift, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CochainComplex.HomComplex.Cochain.leftShift_v, LinearIndependent.units_smul, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, MultilinearMap.alternatization_coe, CochainComplex.HomComplex.Cochain.δ_leftUnshift, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, HomologicalComplex.mapBifunctor.d₁_eq', instFaithfulSMul, TensorProduct.tmul_of_gradedMul_of_tmul, CochainComplex.shiftFunctor_obj_d', FractionalIdeal.spanSingleton_eq_spanSingleton, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.HomComplex.Cochain.leftShift_units_smul, HomologicalComplex.ι_mapBifunctorFlipIso_hom, LinearIndependent.units_smul_iff, Matrix.det_neg_eq_smul, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, map_zsmul_unit, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, HomologicalComplex.mapBifunctor.d₂_eq', AlternatingMap.domDomCongr_perm, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, TensorProduct.gradedCommAux_lof_tmul, CategoryTheory.NatTrans.app_units_zsmul, CochainComplex.mappingCone.δ_descCochain, HomologicalComplex₂.d₂_eq', CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂, HomologicalComplex₂.d₁_eq', continuousSMul, spectrum.unit_smul_eq_smul, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, HomologicalComplex₂.D₁_totalShift₂XIso_hom, HomologicalComplex.mapBifunctor₁₂.d₁_eq, HomologicalComplex₂.D₂_totalShift₂XIso_hom, norm_units_zsmul, Module.Basis.repr_unitsSMul, spectrum.units_smul_resolvent, HomologicalComplex.mapBifunctor₁₂.d₃_eq, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, Module.Basis.units_smul_span_eq_top, TensorProduct.gradedComm_of_tmul_of, exteriorPower.toTensorPower_apply_ιMulti, HomologicalComplex.mapBifunctor₁₂.d₂_eq, Module.Basis.unitsSMul_apply, LinearEquiv.smul_refl, Module.Basis.coord_unitsSMul, CochainComplex.HomComplex.Cochain.δ_leftShift, HomologicalComplex₂.totalAux.d₁_eq', HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc, Submodule.span_singleton_eq_span_singleton, CochainComplex.HomComplex.δ_zero_cochain_comp, isScalarTower'_left, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, HomologicalComplex.mapBifunctor.d₁_eq, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, CochainComplex.shiftFunctor_obj_d, MultilinearMap.alternatization_def, CategoryTheory.ObjectProperty.smul_mem_trW_iff, HomologicalComplex.ι_mapBifunctorFlipIso_inv, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, Matrix.GeneralLinearGroup.fin_two_smul_prod
mulAction' 📖	CompOp	6 math math: smul_inv, val_smul, smulCommClass', isScalarTower', smul_eq_mul, isScalarTower'_left
mulDistribMulActionRight 📖	CompOp	2 math math: coe_smul, coe_inv_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inv_smul 📖	mathematical	—	val Units instInv SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction instMonoid mulDistribMulActionRight	—	—
coe_smul 📖	mathematical	—	val Units SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction instMonoid mulDistribMulActionRight	—	—
instFaithfulSMul 📖	mathematical	—	FaithfulSMul Units instSMul	—	ext FaithfulSMul.eq_of_smul_eq_smul
instIsScalarTower 📖	mathematical	—	IsScalarTower Units instSMul	—	smul_assoc
isScalarTower' 📖	mathematical	—	IsScalarTower Units SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction'	—	ext smul_assoc
isScalarTower'_left 📖	mathematical	—	IsScalarTower Units SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction' instSMul	—	smul_assoc
smulCommClass' 📖	mathematical	—	SMulCommClass Units SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction'	—	ext SMulCommClass.smul_comm
smulCommClass_left 📖	mathematical	—	SMulCommClass Units instSMul	—	SMulCommClass.smul_comm
smulCommClass_right 📖	mathematical	—	SMulCommClass Units instSMul	—	SMulCommClass.smul_comm
smul_def 📖	mathematical	—	Units instSMul val	—	—
smul_eq_mul 📖	mathematical	—	Units CommMonoid.toMonoid SemigroupAction.toSMul Monoid.toSemigroup instMonoid MulAction.toSemigroupAction mulAction' instGroup instMulAction Monoid.toMulAction smulCommClass_left smulCommClass_self instIsScalarTower IsScalarTower.left instMul	—	ext smulCommClass_left smulCommClass_self instIsScalarTower IsScalarTower.left
smul_inv 📖	mathematical	—	Units instInv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction' InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	ext
smul_isUnit 📖	mathematical	IsUnit	Units instSMul IsUnit.unit	—	—
smul_mk_apply 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	Units instSMul	—	—
val_smul 📖	mathematical	—	val Units SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction'	—	—

---

← Back to Index