Faithful

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

Statistics

Metric	Count
Definitions FaithfulSMul, FaithfulVAdd	2
Theorems to_faithfulVAdd_addOpposite, faithfulVAdd, eq_of_smul_eq_smul, tower_bot, trans, eq_of_vadd_eq_vadd, tower_bot, trans, to₁₂₃, to_faithfulSMul_mulOpposite, to_faithfulSMul_mulOpposite, faithfulSMul, to₁₂₃, faithfulSMul_iff, faithfulSMul_iff_injective_smul_one, faithfulVAdd_iff, faithfulVAdd_iff_injective_vadd_zero, instFaithfulSMul, instFaithfulSMulMulOpposite, instFaithfulSMulMulOppositeOfIsLeftCancelMul, instFaithfulSMulMulOpposite_1, instFaithfulSMulOfIsRightCancelMul, instFaithfulVAdd, instFaithfulVAddAddOpposite, instFaithfulVAddAddOppositeOfIsLeftCancelAdd, instFaithfulVAddOfIsRightCancelAdd, smul_left_injective', vadd_left_injective'	28
Total	30

AddLeftCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_faithfulVAdd_addOpposite 📖	mathematical	—	FaithfulVAdd AddOpposite Add.toVAddAddOpposite AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass toAddMonoid	—	instFaithfulVAddAddOppositeOfIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd

AddRightCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithfulVAdd 📖	mathematical	—	FaithfulVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	instFaithfulVAddOfIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd

FaithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_smul_eq_smul 📖	—	—	—	—	—
tower_bot 📖	mathematical	—	FaithfulSMul	—	faithfulSMul_iff_injective_smul_one Function.Injective.of_comp smul_assoc one_smul
trans 📖	mathematical	—	FaithfulSMul	—	smul_assoc one_smul faithfulSMul_iff_injective_smul_one

FaithfulVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_vadd_eq_vadd 📖	—	HVAdd.hVAdd instHVAdd	—	—	—
tower_bot 📖	mathematical	—	FaithfulVAdd	—	faithfulVAdd_iff_injective_vadd_zero Function.Injective.of_comp vadd_assoc zero_vadd
trans 📖	mathematical	—	FaithfulVAdd	—	faithfulVAdd_iff_injective_vadd_zero vadd_assoc zero_vadd

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to₁₂₃ 📖	mathematical	—	IsScalarTower	—	smul_left_injective' smul_assoc

LeftCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_faithfulSMul_mulOpposite 📖	mathematical	—	FaithfulSMul MulOpposite Mul.toSMulMulOpposite MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid	—	instFaithfulSMulMulOppositeOfIsLeftCancelMul LeftCancelSemigroup.toIsLeftCancelMul

LefttCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_faithfulSMul_mulOpposite 📖	mathematical	—	FaithfulSMul MulOpposite Mul.toSMulMulOpposite MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass LeftCancelMonoid.toMonoid	—	LeftCancelMonoid.to_faithfulSMul_mulOpposite

RightCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithfulSMul 📖	mathematical	—	FaithfulSMul SemigroupAction.toSMul Monoid.toSemigroup toMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	instFaithfulSMulOfIsRightCancelMul RightCancelSemigroup.toIsRightCancelMul

VAddAssocClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to₁₂₃ 📖	mathematical	—	VAddAssocClass	—	vadd_left_injective' vadd_assoc

(root)

Definitions

Name	Category	Theorems
FaithfulSMul 📖	CompData	92 math math: RatFunc.instFaithfulSMulPolynomialLaurentSeries, Sum.FaithfulSMulLeft, LefttCancelMonoid.to_faithfulSMul_mulOpposite, Prod.faithfulSMulRight, FaithfulSMul.of_field_isFractionRing, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, faithfulSMul_iff_algebraMap_injective, instFaithfulSMulNatOfCharZero, Module.Free.instFaithfulSMulOfNontrivial, Ideal.Quotient.instFaithfulSMul, Subsemiring.instFaithfulSMulSubtypeMem, Ring.instFaithfulSMulNormalClosure, Pi.faithfulSMul_at, Set.powersetCard.faithfulSMul, DomMulAct.instFaithfulSMulForallOfNontrivial, MvPolynomial.faithfulSMul, NoZeroSMulDivisors.iff_faithfulSMul, LeftCancelMonoid.to_faithfulSMul_mulOpposite, Equiv.faithfulSMul, FaithfulSMul.of_injective, Subring.instFaithfulSMulSubtypeMem, instFaithfulSMulOfIsRightCancelMul, Monoid.PushoutI.NormalWord.instFaithfulSMul, IsFractionRing.instFaithfulSMul, SkewMonoidAlgebra.instFaithfulSMul, MonoidAlgebra.faithfulSMul, ContinuousLinearMap.applyFaithfulSMul, RightCancelMonoid.faithfulSMul, Module.FaithfullyFlat.faithfulSMul, Finsupp.instFaithfulSMulOfNonempty, IsGaloisGroup.faithful, instFaithfulSMulIntOfCharZero, Sum.FaithfulSMulRight, RingHom.applyFaithfulSMul, HNNExtension.NormalWord.instFaithfulSMul_1, RelEmbedding.apply_faithfulSMul, Equiv.Perm.applyFaithfulSMul, Subfield.instFaithfulSMulSubtypeMem, HNNExtension.NormalWord.instFaithfulSMul, IntermediateField.instFaithfulSMulSubtypeMem, Submonoid.faithfulSMul, AddMonoidAlgebra.faithfulSMul, RelIso.apply_faithfulSMul, RatFunc.faithfulSMul, Module.IsTorsionFree.to_faithfulSMul, Subalgebra.instFaithfulSMulSubtypeMem, Sigma.FaithfulSMul', IsLeftCancelMulZero.toFaithfulSMul_opposite, AddAut.apply_faithfulSMul, Subalgebra.inclusion.faithfulSMul, AddMonoid.End.applyFaithfulSMul, Module.isTorsionFree_iff_faithfulSMul, Algebra.Presentation.instFaithfulSMulCore, Prod.faithfulSMulLeft, Module.annihilator_eq_bot, instFaithfulSMul, instFaithfulSMul_1, Module.Invertible.instFaithfulSMul, IsAzumaya.toFaithfulSMul, Module.End.apply_faithfulSMul, instFaithfulSMulPolynomial, Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors, Units.instFaithfulSMul, faithfulSMul_iff_injective_smul_one, IsRightCancelMulZero.faithfulSMul, IsLocalization.AtPrime.faithfulSMul, faithfulSMul_iff, FaithfulSMul.trans, Monoid.PushoutI.NormalWord.instFaithfulSMul_2, AlgEquiv.apply_faithfulSMul, Valued.instFaithfulSMulCompletionOfUniformContinuousConstSMul, Polynomial.faithfulSMul, RingAut.apply_faithfulSMul, Option.instFaithfulSMul, instFaithfulSMulMulOpposite_1, IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, Finsupp.faithfulSMul, MulAut.apply_faithfulSMul, Algebra.IsAlgebraic.faithfulSMul_tower_top, RelHom.apply_faithfulSMul, FractionRing.instFaithfulSMul, instFaithfulSMulMulOppositeOfIsLeftCancelMul, FaithfulSMul.tower_bot, Subsemiring.faithfulSMul, Monoid.PushoutI.NormalWord.instFaithfulSMul_1, Subgroup.instFaithfulSMulSubtypeMem, RegularWreathProduct.instFaithfulSMulProdOfNonempty, instFaithfulSMulMulOpposite, LinearEquiv.apply_faithfulSMul, MvPolynomial.instFaithfulSMul, Function.End.apply_FaithfulSMul
FaithfulVAdd 📖	CompData	24 math math: Equiv.faithfulVAdd, Sigma.FaithfulVAdd', instFaithfulVAddAddOpposite, FaithfulVAdd.tower_bot, Option.instFaithfulVAdd, AddUnits.instFaithfulVAdd, Prod.faithfulVAddRight, AddSubgroup.instFaithfulVAddSubtypeMem, Set.powersetCard.faithfulVAdd, faithfulVAdd_iff_injective_vadd_zero, Sum.FaithfulVAddRight, Prod.faithfulVAddLeft, Pi.faithfulVAdd_at, DomAddAct.instFaithfulVAddForallOfNontrivial, AddSubmonoid.faithfulVAdd, AddRightCancelMonoid.faithfulVAdd, instFaithfulVAddAddOppositeOfIsLeftCancelAdd, AddLeftCancelMonoid.to_faithfulVAdd_addOpposite, faithfulVAdd_iff, Submodule.instFaithfulVAddSubtypeMem, instFaithfulVAddOfIsRightCancelAdd, FaithfulVAdd.trans, instFaithfulVAdd, Sum.FaithfulVAddLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithfulSMul_iff 📖	mathematical	—	FaithfulSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	FaithfulSMul.eq_of_smul_eq_smul one_smul inv_inv eq_inv_of_mul_eq_one_left SemigroupAction.mul_smul
faithfulSMul_iff_injective_smul_one 📖	mathematical	—	FaithfulSMul MulOne.toOne MulOneClass.toMulOne	—	one_mul smul_mul_assoc
faithfulVAdd_iff 📖	mathematical	—	FaithfulVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	FaithfulVAdd.eq_of_vadd_eq_vadd zero_vadd neg_neg eq_neg_of_add_eq_zero_left AddSemigroupAction.add_vadd neg_vadd_eq_iff
faithfulVAdd_iff_injective_vadd_zero 📖	mathematical	—	FaithfulVAdd HVAdd.hVAdd instHVAdd AddZero.toZero AddZeroClass.toAddZero	—	zero_add vadd_add_assoc
instFaithfulSMul 📖	mathematical	—	FaithfulSMul MulOne.toMul MulOneClass.toMulOne	—	mul_one
instFaithfulSMulMulOpposite 📖	mathematical	—	FaithfulSMul MulOpposite Mul.toSMulMulOpposite MulOne.toMul MulOneClass.toMulOne	—	one_mul
instFaithfulSMulMulOppositeOfIsLeftCancelMul 📖	mathematical	—	FaithfulSMul MulOpposite Mul.toSMulMulOpposite	—	—
instFaithfulSMulMulOpposite_1 📖	mathematical	—	FaithfulSMul MulOpposite MulOpposite.instSMul	—	FaithfulSMul.eq_of_smul_eq_smul
instFaithfulSMulOfIsRightCancelMul 📖	mathematical	—	FaithfulSMul	—	—
instFaithfulVAdd 📖	mathematical	—	FaithfulVAdd Add.toVAdd AddZero.toAdd AddZeroClass.toAddZero	—	add_zero
instFaithfulVAddAddOpposite 📖	mathematical	—	FaithfulVAdd AddOpposite Add.toVAddAddOpposite AddZero.toAdd AddZeroClass.toAddZero	—	zero_add
instFaithfulVAddAddOppositeOfIsLeftCancelAdd 📖	mathematical	—	FaithfulVAdd AddOpposite Add.toVAddAddOpposite	—	—
instFaithfulVAddOfIsRightCancelAdd 📖	mathematical	—	FaithfulVAdd Add.toVAdd	—	—
smul_left_injective' 📖	—	—	—	—	FaithfulSMul.eq_of_smul_eq_smul
vadd_left_injective' 📖	mathematical	—	HVAdd.hVAdd instHVAdd	—	FaithfulVAdd.eq_of_vadd_eq_vadd

---

← Back to Index