Basic

📁 Source: Mathlib/Algebra/Order/Hom/Basic.lean

Statistics

Metric	Count
Definitions AddGroupNormClass, AddGroupSeminormClass, GroupNormClass, GroupSeminormClass, «out-param_inheritance», MulLEAddHomClass, MulRingNormClass, MulRingSeminormClass, NonarchimedeanHomClass, NonnegHomClass, RingNormClass, RingSeminormClass, SubadditiveHomClass, SubmultiplicativeHomClass	14
Theorems eq_zero_of_map_eq_zero, toAddGroupSeminormClass, map_neg_eq_map, map_zero, toNonnegHomClass, toSubadditiveHomClass, toZeroHomClass, eq_one_of_map_eq_zero, toGroupSeminormClass, map_inv_eq_map, map_one_eq_zero, toMulLEAddHomClass, toNonnegHomClass, map_mul_le_add, eq_zero_of_map_eq_zero, toAddGroupNormClass, toMulRingSeminormClass, toRingNormClass, toAddGroupSeminormClass, toMonoidHomClass, toMonoidWithZeroHomClass, toRingSeminormClass, map_add_le_max, apply_nonneg, eq_zero_of_map_eq_zero, toAddGroupNormClass, toRingSeminormClass, toAddGroupSeminormClass, toNonnegHomClass, toSubmultiplicativeHomClass, map_add_le_add, map_mul_le_mul, abs_sub_map_le_div, abs_sub_map_le_sub, le_map_add_map_div, le_map_add_map_div', le_map_add_map_sub, le_map_add_map_sub', le_map_div_add_map_div, le_map_div_mul_map_div, le_map_mul_map_div, le_map_sub_add_map_sub, map_div_le_add, map_div_rev, map_eq_zero_iff_eq_one, map_eq_zero_iff_eq_zero, map_ne_zero_iff_ne_one, map_ne_zero_iff_ne_zero, map_pos_of_ne_one, map_pos_of_ne_zero, map_sub_le_add, map_sub_rev	52
Total	66

AddGroupNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_map_eq_zero 📖	mathematical	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
toAddGroupSeminormClass 📖	mathematical	—	AddGroupSeminormClass	—	—

AddGroupSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_neg_eq_map 📖	mathematical	—	DFunLike.coe NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
map_zero 📖	mathematical	—	DFunLike.coe NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
toNonnegHomClass 📖	mathematical	—	NonnegHomClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nsmul_nonneg_iff IsOrderedAddMonoid.toAddLeftMono two_ne_zero two_nsmul map_zero sub_self map_sub_le_add
toSubadditiveHomClass 📖	mathematical	—	SubadditiveHomClass AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	—	—
toZeroHomClass 📖	mathematical	—	ZeroHomClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero

GroupNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one_of_map_eq_zero 📖	mathematical	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
toGroupSeminormClass 📖	mathematical	—	GroupSeminormClass	—	—

GroupSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_inv_eq_map 📖	mathematical	—	DFunLike.coe InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
map_one_eq_zero 📖	mathematical	—	DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
toMulLEAddHomClass 📖	mathematical	—	MulLEAddHomClass MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	—	—
toNonnegHomClass 📖	mathematical	—	NonnegHomClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nsmul_nonneg_iff IsOrderedAddMonoid.toAddLeftMono two_ne_zero two_nsmul map_one_eq_zero div_self' map_div_le_add

LibraryNote

Definitions

Name	Category	Theorems
«out-param_inheritance» 📖	CompOp	—

MulLEAddHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_le_add 📖	mathematical	—	DFunLike.coe	—	—

MulRingNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_map_eq_zero 📖	mathematical	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	—
toAddGroupNormClass 📖	mathematical	—	AddGroupNormClass AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	MulRingSeminormClass.toAddGroupSeminormClass toMulRingSeminormClass eq_zero_of_map_eq_zero
toMulRingSeminormClass 📖	mathematical	—	MulRingSeminormClass	—	—
toRingNormClass 📖	mathematical	—	RingNormClass NonAssocRing.toNonUnitalNonAssocRing	—	MulRingSeminormClass.toRingSeminormClass toMulRingSeminormClass MulRingSeminormClass.toAddGroupSeminormClass RingSeminormClass.toSubmultiplicativeHomClass eq_zero_of_map_eq_zero

MulRingSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddGroupSeminormClass 📖	mathematical	—	AddGroupSeminormClass AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toMonoidHomClass 📖	mathematical	—	MonoidHomClass MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass NonAssocRing.toNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toMonoidWithZeroHomClass 📖	mathematical	—	MonoidWithZeroHomClass NonAssocSemiring.toMulZeroOneClass NonAssocRing.toNonAssocSemiring Semiring.toNonAssocSemiring	—	toMonoidHomClass AddGroupSeminormClass.map_zero toAddGroupSeminormClass
toRingSeminormClass 📖	mathematical	—	RingSeminormClass NonAssocRing.toNonUnitalNonAssocRing	—	toAddGroupSeminormClass Eq.le map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass toMonoidWithZeroHomClass

NonarchimedeanHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—

NonnegHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_nonneg 📖	mathematical	—	DFunLike.coe	—	—

RingNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_map_eq_zero 📖	mathematical	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	—
toAddGroupNormClass 📖	mathematical	—	AddGroupNormClass AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	RingSeminormClass.toAddGroupSeminormClass toRingSeminormClass eq_zero_of_map_eq_zero
toRingSeminormClass 📖	mathematical	—	RingSeminormClass	—	—

RingSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddGroupSeminormClass 📖	mathematical	—	AddGroupSeminormClass AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
toNonnegHomClass 📖	mathematical	—	NonnegHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	AddGroupSeminormClass.toNonnegHomClass toAddGroupSeminormClass
toSubmultiplicativeHomClass 📖	mathematical	—	SubmultiplicativeHomClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder	—	—

SubadditiveHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_le_add 📖	mathematical	—	DFunLike.coe	—	—

SubmultiplicativeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_le_mul 📖	mathematical	—	DFunLike.coe	—	—

(root)

Definitions

Name	Category	Theorems
AddGroupNormClass 📖	CompData	4 math math: RingNormClass.toAddGroupNormClass, MulRingNormClass.toAddGroupNormClass, AddGroupNorm.addGroupNormClass, NonarchAddGroupNormClass.toAddGroupNormClass
AddGroupSeminormClass 📖	CompData	6 math math: AddGroupNormClass.toAddGroupSeminormClass, NonarchAddGroupSeminormClass.toAddGroupSeminormClass, AddGroupSeminorm.addGroupSeminormClass, SeminormClass.toAddGroupSeminormClass, RingSeminormClass.toAddGroupSeminormClass, MulRingSeminormClass.toAddGroupSeminormClass
GroupNormClass 📖	CompData	1 math math: GroupNorm.groupNormClass
GroupSeminormClass 📖	CompData	2 math math: GroupNormClass.toGroupSeminormClass, GroupSeminorm.groupSeminormClass
MulLEAddHomClass 📖	CompData	1 math math: GroupSeminormClass.toMulLEAddHomClass
MulRingNormClass 📖	CompData	3 math math: MulAlgebraNormClass.toMulRingNormClass, MulRingNorm.mulRingNormClass, AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain
MulRingSeminormClass 📖	CompData	2 math math: MulRingNormClass.toMulRingSeminormClass, MulRingSeminorm.mulRingSeminormClass
NonarchimedeanHomClass 📖	CompData	2 math math: NonarchAddGroupSeminormClass.toNonarchimedeanHomClass, NumberField.FinitePlace.instNonarchimedeanHomClassReal
NonnegHomClass 📖	CompData	6 math math: AddGroupSeminormClass.toNonnegHomClass, GroupSeminormClass.toNonnegHomClass, NumberField.FinitePlace.instNonnegHomClassReal, RingSeminormClass.toNonnegHomClass, AbsoluteValue.nonnegHomClass, NumberField.InfinitePlace.instNonnegHomClassReal
RingNormClass 📖	CompData	3 math math: MulRingNormClass.toRingNormClass, AlgebraNormClass.toRingNormClass, RingNorm.ringNormClass
RingSeminormClass 📖	CompData	3 math math: RingSeminorm.ringSeminormClass, MulRingSeminormClass.toRingSeminormClass, RingNormClass.toRingSeminormClass
SubadditiveHomClass 📖	CompData	2 math math: AddGroupSeminormClass.toSubadditiveHomClass, AbsoluteValue.subadditiveHomClass
SubmultiplicativeHomClass 📖	CompData	1 math math: RingSeminormClass.toSubmultiplicativeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_sub_map_le_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid DFunLike.coe DivInvMonoid.toDiv Group.toDivInvMonoid	—	abs_sub_le_iff sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono le_map_add_map_div GroupSeminormClass.toMulLEAddHomClass le_map_add_map_div'
abs_sub_map_le_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid DFunLike.coe	—	abs_sub_le_iff sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono le_map_add_map_sub AddGroupSeminormClass.toSubadditiveHomClass le_map_add_map_sub'
le_map_add_map_div 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_mul_cancel add_comm MulLEAddHomClass.map_mul_le_add
le_map_add_map_div' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	map_div_rev div_mul_cancel add_comm MulLEAddHomClass.map_mul_le_add GroupSeminormClass.toMulLEAddHomClass
le_map_add_map_sub 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_add_cancel add_comm SubadditiveHomClass.map_add_le_add
le_map_add_map_sub' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	map_sub_rev sub_add_cancel add_comm SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass
le_map_div_add_map_div 📖	mathematical	—	DFunLike.coe DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_mul_div_cancel MulLEAddHomClass.map_mul_le_add
le_map_div_mul_map_div 📖	mathematical	—	DFunLike.coe DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_mul_div_cancel SubmultiplicativeHomClass.map_mul_le_mul
le_map_mul_map_div 📖	mathematical	—	DFunLike.coe CommMagma.toMul DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_mul_cancel mul_comm SubmultiplicativeHomClass.map_mul_le_mul
le_map_sub_add_map_sub 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_add_sub_cancel SubadditiveHomClass.map_add_le_add
map_div_le_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe DivInvMonoid.toDiv Group.toDivInvMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	div_eq_mul_inv GroupSeminormClass.map_inv_eq_map MulLEAddHomClass.map_mul_le_add GroupSeminormClass.toMulLEAddHomClass
map_div_rev 📖	mathematical	—	DFunLike.coe DivInvMonoid.toDiv Group.toDivInvMonoid	—	inv_div GroupSeminormClass.map_inv_eq_map
map_eq_zero_iff_eq_one 📖	mathematical	—	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	GroupNormClass.eq_one_of_map_eq_zero GroupSeminormClass.map_one_eq_zero GroupNormClass.toGroupSeminormClass
map_eq_zero_iff_eq_zero 📖	mathematical	—	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	AddGroupNormClass.eq_zero_of_map_eq_zero AddGroupSeminormClass.map_zero AddGroupNormClass.toAddGroupSeminormClass
map_ne_zero_iff_ne_one 📖	—	—	—	—	Iff.not map_eq_zero_iff_eq_one
map_ne_zero_iff_ne_zero 📖	—	—	—	—	Iff.not map_eq_zero_iff_eq_zero
map_pos_of_ne_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe	—	LE.le.lt_of_ne NonnegHomClass.apply_nonneg GroupSeminormClass.toNonnegHomClass GroupNormClass.toGroupSeminormClass map_ne_zero_iff_ne_one
map_pos_of_ne_zero 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe	—	LE.le.lt_of_ne NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass AddGroupNormClass.toAddGroupSeminormClass map_ne_zero_iff_ne_zero
map_sub_le_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	sub_eq_add_neg AddGroupSeminormClass.map_neg_eq_map SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass
map_sub_rev 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	neg_sub AddGroupSeminormClass.map_neg_eq_map

---

← Back to Index