IndexNormal

Statistics

Metric	Count
Definitions	0
Theorems `normal_of_index_eq_minFac_card`, `normal_of_index_eq_one`, `normal_of_index_eq_two`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_of_index_eq_minFac_card` 📖	mathematical	`index` `Nat.minFac` `Nat.card`	`Normal`	—	`normal_of_index_eq_two` `Nat.minFac_zero` `normal_of_index_eq_one` `Nat.minFac_one` `Nat.finite_of_card_ne_zero` `index_ne_zero_of_finite` `finite_quotient_of_finiteIndex` `finiteIndex_of_finite` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `one_mul` `relIndex_mul_index` `normalCore_le` `Nat.minFac_prime` `MulAction.left_quotientAction` `normalCore_eq_ker` `index_ker` `index_eq_card` `Nat.card_perm` `card_subgroup_dvd_card` `dvd_antisymm` `Unique.instSubsingleton` `Nat.Coprime.dvd_mul_right` `Nat.Prime.ne_one` `index_dvd_of_le` `Nat.coprime_factorial_iff` `lt_of_lt_of_le` `Nat.Prime.ne_zero` `Nat.minFac_le_of_dvd` `Nat.Prime.two_le` `dvd_trans` `Nat.minFac_dvd` `index_dvd_card` `Nat.mul_factorial_pred` `le_antisymm` `relIndex_eq_one` `normalCore_normal`
`normal_of_index_eq_one` 📖	mathematical	`index`	`Normal`	—	`index_eq_one` `normal_top`
`normal_of_index_eq_two` 📖	mathematical	`index`	`Normal`	—	`mul_mem_iff_of_index_two` `SubgroupClass.toInvMemClass` `instSubgroupClass`

---