CharacterModule

📁 Source: Mathlib/Algebra/Module/CharacterModule.lean

Statistics

Metric	Count
Definitions CharacterModule, curry, dual, homEquiv, instAddCommGroup, instFunLikeAddCircleRatOfNat, instModule, int, divByNat, intSpanEquivQuotAddOrderOf, ofSpanSingleton, uncurry	12
Theorems curry_apply_apply, dual_apply, dual_bijective_iff_bijective, dual_comp, dual_injective_iff_surjective, dual_injective_of_surjective, dual_rTensor_conj_homEquiv, dual_surjective_iff_injective, dual_surjective_of_injective, dual_zero, eq_zero_of_character_apply, eq_zero_of_ofSpanSingleton_apply_self, exists_character_apply_ne_zero_of_ne_zero, ext, ext_iff, homEquiv_apply_apply, homEquiv_symm_apply_apply_apply, instLinearMapClassIntAddCircleRatOfNat, divByNat_self, intSpanEquivQuotAddOrderOf_apply, intSpanEquivQuotAddOrderOf_apply_self, intSpanEquivQuotAddOrderOf_symm_apply_coe, smul_apply, surjective_of_dual_injective, uncurry_apply, rTensor_injective_iff_lcomp_surjective	26
Total	38

CharacterModule

Definitions

Name	Category	Theorems
curry 📖	CompOp	1 math math: curry_apply_apply
dual 📖	CompOp	9 math math: dual_injective_of_surjective, dual_comp, dual_surjective_of_injective, dual_bijective_iff_bijective, dual_rTensor_conj_homEquiv, dual_surjective_iff_injective, dual_zero, dual_apply, dual_injective_iff_surjective
homEquiv 📖	CompOp	3 math math: homEquiv_symm_apply_apply_apply, dual_rTensor_conj_homEquiv, homEquiv_apply_apply
instAddCommGroup 📖	CompOp	18 math math: dual_injective_of_surjective, rTensor_injective_iff_lcomp_surjective, smul_apply, curry_apply_apply, dual_comp, dual_surjective_of_injective, homEquiv_symm_apply_apply_apply, dual_bijective_iff_bijective, dual_rTensor_conj_homEquiv, uncurry_apply, dual_surjective_iff_injective, dual_zero, homEquiv_apply_apply, Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap, dual_apply, Module.Flat.iff_characterModule_baer, dual_injective_iff_surjective, Module.Flat.iff_characterModule_injective
instFunLikeAddCircleRatOfNat 📖	CompOp	4 math math: int.divByNat_self, smul_apply, instLinearMapClassIntAddCircleRatOfNat, ext_iff
instModule 📖	CompOp	18 math math: dual_injective_of_surjective, rTensor_injective_iff_lcomp_surjective, smul_apply, curry_apply_apply, dual_comp, dual_surjective_of_injective, homEquiv_symm_apply_apply_apply, dual_bijective_iff_bijective, dual_rTensor_conj_homEquiv, uncurry_apply, dual_surjective_iff_injective, dual_zero, homEquiv_apply_apply, Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap, dual_apply, Module.Flat.iff_characterModule_baer, dual_injective_iff_surjective, Module.Flat.iff_characterModule_injective
int 📖	CompOp	1 math math: int.divByNat_self
intSpanEquivQuotAddOrderOf 📖	CompOp	3 math math: intSpanEquivQuotAddOrderOf_symm_apply_coe, intSpanEquivQuotAddOrderOf_apply, intSpanEquivQuotAddOrderOf_apply_self
ofSpanSingleton 📖	CompOp	—
uncurry 📖	CompOp	1 math math: uncurry_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curry_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CharacterModule AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike TensorProduct TensorProduct.addCommGroup LinearMap.addCommMonoid TensorProduct.instModule LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing curry AddMonoidHom.comp AddCircle Rat.addCommGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddMonoidHomClass.toAddMonoidHom TensorProduct.addCommMonoid	—	smulCommClass_self
dual_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CharacterModule AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike dual AddMonoidHom.comp AddCircle Rat.addCommGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples LinearMap.toAddMonoidHom	—	—
dual_bijective_iff_bijective 📖	mathematical	—	Function.Bijective CharacterModule DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike dual	—	dual_surjective_iff_injective dual_injective_iff_surjective
dual_comp 📖	mathematical	—	dual LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CharacterModule instAddCommGroup instModule	—	LinearMap.ext RingHomCompTriple.ids ext
dual_injective_iff_surjective 📖	mathematical	—	CharacterModule DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike dual	—	surjective_of_dual_injective dual_injective_of_surjective
dual_injective_of_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	CharacterModule instAddCommGroup instModule dual	—	ext
dual_rTensor_conj_homEquiv 📖	mathematical	—	LinearMap.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CharacterModule AddCommGroup.toAddCommMonoid instAddCommGroup instModule TensorProduct TensorProduct.addCommGroup LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing TensorProduct.instModule RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm homEquiv dual LinearMap.rTensor LinearMap.lcomp	—	smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids
dual_surjective_iff_injective 📖	mathematical	—	CharacterModule DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike dual	—	injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass eq_zero_of_character_apply AddMonoidHom.map_zero dual_surjective_of_injective
dual_surjective_of_injective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	CharacterModule instAddCommGroup instModule dual	—	Module.Baer.extension_property_addMonoidHom Module.Baer.of_divisible Rat.instIsStrictOrderedRing ZeroLEOneClass.factZeroLtOne Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero
dual_zero 📖	mathematical	—	dual LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero CharacterModule instAddCommGroup instModule	—	LinearMap.ext ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass instLinearMapClassIntAddCircleRatOfNat
eq_zero_of_character_apply 📖	—	DFunLike.coe CharacterModule AddCircle Rat.addCommGroup instFunLikeAddCircleRatOfNat NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq exists_character_apply_ne_zero_of_ne_zero
eq_zero_of_ofSpanSingleton_apply_self 📖	—	DFunLike.coe CharacterModule Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet Submodule.addCommGroup Int.instRing AddCircle Rat.addCommGroup instFunLikeAddCircleRatOfNat ofSpanSingleton Submodule.mem_span_singleton_self NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup	—	—	Submodule.mem_span_singleton_self AddCircle.coe_eq_zero_iff LinearMap.toSpanSingleton_apply_one int.divByNat.eq_1 AddMonoidHom.coe_toIntLinearMap Submodule.liftQSpanSingleton_apply RingHomInvPair.ids intSpanEquivQuotAddOrderOf_apply_self LinearMap.comp_apply LinearMap.toAddMonoidHom_coe ofSpanSingleton.eq_1 Rat.inv_natCast_den_of_pos zsmul_one AddMonoid.addOrderOf_eq_one_iff
exists_character_apply_ne_zero_of_ne_zero 📖	—	—	—	—	dual_surjective_of_injective Submodule.injective_subtype eq_zero_of_ofSpanSingleton_apply_self Submodule.mem_span_singleton_self
ext 📖	—	DFunLike.coe CharacterModule AddCircle Rat.addCommGroup instFunLikeAddCircleRatOfNat	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CharacterModule AddCircle Rat.addCommGroup instFunLikeAddCircleRatOfNat	—	ext
homEquiv_apply_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCircle Rat.addCommGroup AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup AddMonoidHom.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap CharacterModule instAddCommGroup instModule TensorProduct.addCommGroup LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike homEquiv AddCon.liftOn FreeAddMonoid AddZero.toAdd AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid FreeAddMonoid.instAddCancelMonoid addConGen AddSemigroup.toAdd AddMonoid.toAddSemigroup TensorProduct.Eqv Equiv Equiv.instEquivLike FreeAddMonoid.lift AddMonoidHom.instAddCommMonoid LinearMap.toAddMonoidHom	—	RingHomInvPair.ids smulCommClass_self
homEquiv_symm_apply_apply_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddCircle Rat.addCommGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddMonoidHom.instFunLike LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CharacterModule AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids TensorProduct TensorProduct.addCommGroup LinearMap.addCommMonoid TensorProduct.instModule LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm homEquiv TensorProduct.tmul	—	RingHomInvPair.ids smulCommClass_self
instLinearMapClassIntAddCircleRatOfNat 📖	mathematical	—	LinearMapClass CharacterModule AddCircle Rat.addCommGroup Int.instSemiring AddCommGroup.toAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup AddCommGroup.toIntModule instFunLikeAddCircleRatOfNat	—	AddMonoidHom.map_add AddMonoidHom.map_zsmul RingHom.id_apply
intSpanEquivQuotAddOrderOf_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet HasQuotient.Quotient Ideal Submodule.hasQuotient Int.instRing Int.instAddCommGroup Semiring.toModule Ideal.span addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addCommMonoid Submodule.Quotient.addCommGroup Submodule.addCommGroup EquivLike.toFunLike LinearEquiv.instEquivLike intSpanEquivQuotAddOrderOf Ring.toSemiring LinearMap.ker LinearMap.toSpanSingleton Submodule.Quotient.module Submodule.quotEquivOfEq LinearMap.range NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring RingHomSurjective.ids Submodule.module LinearEquiv.symm LinearMap.quotKerEquivRange LinearEquiv.ofEq	—	RingHomInvPair.ids
intSpanEquivQuotAddOrderOf_apply_self 📖	mathematical	—	DFunLike.coe LinearEquiv Int.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet HasQuotient.Quotient Ideal Submodule.hasQuotient Int.instRing Int.instAddCommGroup Semiring.toModule Ideal.span addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addCommMonoid Submodule.Quotient.addCommGroup Submodule.addCommGroup EquivLike.toFunLike LinearEquiv.instEquivLike intSpanEquivQuotAddOrderOf Submodule.mem_span_singleton_self	—	Submodule.mem_span_singleton_self RingHomInvPair.ids LinearEquiv.eq_symm_apply one_zsmul
intSpanEquivQuotAddOrderOf_symm_apply_coe 📖	mathematical	—	Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Ideal Submodule.hasQuotient Int.instRing Int.instAddCommGroup Semiring.toModule Ideal.span addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.Quotient.addCommGroup Submodule.addCommMonoid Submodule.addCommGroup EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm intSpanEquivQuotAddOrderOf Set.instMembership SetLike.coe LinearMap.range NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring RingHomSurjective.ids LinearMap.toSpanSingleton Ring.toSemiring LinearMap.ker Submodule.Quotient.module Submodule.module LinearMap.quotKerEquivRange Submodule.quotEquivOfEq	—	RingHomInvPair.ids
smul_apply 📖	mathematical	—	DFunLike.coe CharacterModule AddCircle Rat.addCommGroup instFunLikeAddCircleRatOfNat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule	—	—
surjective_of_dual_injective 📖	—	CharacterModule DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule LinearMap.instFunLike dual	—	—	RingHomSurjective.ids LinearMap.range_eq_top Submodule.unique_quotient_iff_eq_top eq_zero_of_character_apply AddSubgroup.normal_of_comm QuotientAddGroup.mk'_surjective RingHomCompTriple.ids LinearMap.comp_apply dual_comp RingHomCompTriple.right_ids LinearMap.range_mkQ_comp dual_zero LinearMap.zero_apply dual_apply AddMonoidHom.zero_comp
uncurry_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CharacterModule AddCommGroup.toAddCommMonoid instAddCommGroup instModule TensorProduct TensorProduct.addCommGroup LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing TensorProduct.instModule LinearMap.instFunLike uncurry TensorProduct.liftAddHom AddCircle Rat.addCommGroup QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup LinearMap.toAddMonoidHom	—	smulCommClass_self

CharacterModule.int

Definitions

Name	Category	Theorems
divByNat 📖	CompOp	1 math math: divByNat_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divByNat_self 📖	mathematical	—	DFunLike.coe CharacterModule.int AddCircle Rat.addCommGroup CharacterModule.instFunLikeAddCircleRatOfNat Int.instAddCommGroup divByNat NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup	—	eq_or_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass CharacterModule.instLinearMapClassIntAddCircleRatOfNat AddCircle.coe_eq_zero_iff one_smul zsmul_eq_mul Int.cast_natCast mul_inv_cancel₀ Nat.cast_ne_zero Rat.instCharZero

(root)

Definitions

Name	Category	Theorems
CharacterModule 📖	CompOp	20 math math: CharacterModule.dual_injective_of_surjective, rTensor_injective_iff_lcomp_surjective, CharacterModule.smul_apply, CharacterModule.instLinearMapClassIntAddCircleRatOfNat, CharacterModule.curry_apply_apply, CharacterModule.dual_comp, CharacterModule.dual_surjective_of_injective, CharacterModule.ext_iff, CharacterModule.homEquiv_symm_apply_apply_apply, CharacterModule.dual_bijective_iff_bijective, CharacterModule.dual_rTensor_conj_homEquiv, CharacterModule.uncurry_apply, CharacterModule.dual_surjective_iff_injective, CharacterModule.dual_zero, CharacterModule.homEquiv_apply_apply, Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap, CharacterModule.dual_apply, Module.Flat.iff_characterModule_baer, CharacterModule.dual_injective_iff_surjective, Module.Flat.iff_characterModule_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rTensor_injective_iff_lcomp_surjective 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor CharacterModule CharacterModule.instAddCommGroup CharacterModule.instModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.lcomp	—	smulCommClass_self RingHomInvPair.ids

---

← Back to Index