FixedPointFree

📁 Source: Mathlib/GroupTheory/FixedPointFree.lean

Statistics

Metric	Count
Definitions FixedPointFree, commGroupOfInvolutive, commutatorMap	3
Theorems coe_eq_inv_of_involutive, coe_eq_inv_of_sq_eq_one, commutatorMap_injective, commutatorMap_surjective, commute_all_of_involutive, odd_card_of_involutive, odd_orderOf_of_involutive, orderOf_ne_two_of_involutive, prod_pow_eq_one, commutatorMap_apply	10
Total	13

MonoidHom

Definitions

Name	Category	Theorems
FixedPointFree 📖	MathDef	—
commutatorMap 📖	CompOp	3 math math: FixedPointFree.commutatorMap_surjective, commutatorMap_apply, FixedPointFree.commutatorMap_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutatorMap_apply 📖	mathematical	—	commutatorMap	—	—

MonoidHom.FixedPointFree

Definitions

Name	Category	Theorems
commGroupOfInvolutive 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_inv_of_involutive 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Function.Involutive	InvOneClass.toInv	—	coe_eq_inv_of_sq_eq_one
coe_eq_inv_of_sq_eq_one 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nat.iterate	InvOneClass.toInv	—	Function.iterate_one mul_one prod_pow_eq_one inv_eq_iff_mul_eq_one
commutatorMap_injective 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	MonoidHom.commutatorMap DivInvMonoid.toDiv Group.toDivInvMonoid	—	inv_mul_eq_one map_mul MonoidHomClass.toMulHomClass map_inv eq_inv_mul_iff_mul_eq mul_assoc eq_div_iff_mul_eq' division_def
commutatorMap_surjective 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	MonoidHom.commutatorMap DivInvMonoid.toDiv Group.toDivInvMonoid	—	Finite.surjective_of_injective commutatorMap_injective
commute_all_of_involutive 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Function.Involutive	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	map_mul MonoidHomClass.toMulHomClass inv_inv mul_inv_rev inv_eq_iff_eq_inv coe_eq_inv_of_involutive
odd_card_of_involutive 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Function.Involutive	Odd Nat.instSemiring Nat.card	—	exists_prime_orderOf_dvd_card Nat.fact_prime_two Nat.instAtLeastTwoHAddOfNat Nat.card_eq_fintype_card even_iff_two_dvd Nat.not_odd_iff_even orderOf_ne_two_of_involutive
odd_orderOf_of_involutive 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Function.Involutive	Odd Nat.instSemiring orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Odd.of_dvd_nat odd_card_of_involutive orderOf_dvd_natCard
orderOf_ne_two_of_involutive 📖	—	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Function.Involutive	—	—	coe_eq_inv_of_involutive inv_eq_iff_mul_eq_one sq pow_orderOf_eq_one orderOf_one
prod_pow_eq_one 📖	mathematical	MonoidHom.FixedPointFree DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Nat.iterate	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	commutatorMap_surjective iterate_map_div List.prod_range_div' Function.iterate_zero_apply div_self'

---

← Back to Index