HenselPolynomial

📁 Source: ClassFieldTheory/Mathlib/RingTheory/HenselPolynomial.lean

Statistics

Metric	Count
Definitions `MonicCoprimeFactors`, `congr`, `fst`, `fstOne`, `instUniqueOfSubsingleton`, `liftAdic`, `liftFactorPow`, `map`, `mapEquiv`, `snd`, `sndOne`, `swap`, `toMonicFactors`, `MonicFactors`, `fst`, `fstOne`, `instUniqueOfSubsingleton`, `map`, `snd`, `sndOne`, `instUniqueMonicCoprimeFactorsOfNat`, `instUniqueMonicFactorsOfNat`, `limit`	23
Theorems `ker_factorPow_pow`, `map_le_nilradical`, `ker_factor`, `ker_factorPow`, `degree_mul'`, `coe_liftFactorPow`, `coe_mapEquiv`, `coe_mapEquiv_symm`, `congr_apply_fst`, `congr_apply_snd`, `congr_rfl`, `congr_symm`, `congr_symm_apply_fst`, `congr_symm_apply_snd`, `congr_trans`, `coprime_fst_snd`, `degree_fst_map`, `degree_snd_map`, `ext`, `ext_iff`, `fstOne_eq_sndOne_iff`, `fstOne_fst_toFinsupp_apply`, `fstOne_fst_toFinsupp_support`, `fstOne_snd`, `fst_map_factorPowSucc_liftFactorPow`, `fst_mul_snd_eq`, `instIsLocalHomQuotientIdealRingHomMk`, `instSubsingletonQuotientIdealHPowOfNat`, `liftAdic_injective`, `liftFactorPow_fst`, `liftFactorPow_snd`, `mapEquiv_apply_fst`, `mapEquiv_apply_snd`, `mapEquiv_symm_apply_fst`, `mapEquiv_symm_apply_snd`, `map_bijective_of_isNilpotent`, `map_bijective_of_isNilpotent_ker`, `map_bijective_of_sqZero`, `map_bijective_of_sqZero_ker`, `map_comp`, `map_comp_liftAdic`, `map_comp_map`, `map_congr`, `map_factorPowSucc_liftFactorPow`, `map_fst`, `map_fst_liftAdic`, `map_id`, `map_injective_of_sqZero`, `map_snd`, `map_snd_liftAdic`, `map_surjective_of_sqZero`, `monic`, `monic_fst`, `monic_snd`, `natDegree_fst_map`, `natDegree_snd_map`, `sndOne_fst`, `sndOne_snd_toFinsupp_apply`, `sndOne_snd_toFinsupp_support`, `snd_map_factorPowSucc_liftFactorPow`, `swap_fst`, `swap_snd`, `toMonicFactors_fst`, `toMonicFactors_injective`, `toMonicFactors_snd`, `ext`, `ext_iff`, `fstOne_eq_sndOne_iff`, `fstOne_fst_toFinsupp_apply`, `fstOne_fst_toFinsupp_support`, `fstOne_snd`, `fst_mul_snd_eq`, `map_fst`, `map_snd`, `monic_fst`, `monic_snd`, `sndOne_fst`, `sndOne_snd_toFinsupp_apply`, `sndOne_snd_toFinsupp_support`, `coeff_limit_natDegree`, `coeff_sum_C_mul_X_pow`, `degree_add_lt`, `degree_sub_lt'`, `degree_sum_lt'`, `divByMonic_mem_map`, `exists_monic_map`, `forall_monicFactors_of_irreducible`, `forall_monicFactors_of_natDegree_le_one`, `irreducible_iff_card_monicCoprimeFactors`, `irreducible_iff_card_monicFactors`, `irreducible_map_of_irreducible_of_separable_map`, `irreducible_of_forall_monicFactors`, `map_limit`, `modByMonic_mem_map`, `monic_limit`, `natDegree_limit`, `natDegree_sum_lt`, `two_le_card_monicCoprimeFactors`, `two_le_card_monicFactors`	99
Total	122

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_le_nilradical` 📖	—	—	—	—	—

Ideal.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_factorPow_pow` 📖	—	—	—	—	`factorPow.eq_1`

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_factor` 📖	—	—	—	—	—
`ker_factorPow` 📖	—	—	—	—	`Ideal.Quotient.ker_factorPow_pow`

Polynomial

Definitions

Name	Category	Theorems
`MonicCoprimeFactors` 📖	CompData	34 math math: `MonicCoprimeFactors.map_comp_liftAdic`, `MonicCoprimeFactors.coe_mapEquiv`, `MonicCoprimeFactors.snd_map_factorPowSucc_liftFactorPow`, `MonicCoprimeFactors.congr_trans`, `MonicCoprimeFactors.map_bijective_of_sqZero_ker`, `MonicCoprimeFactors.coe_mapEquiv_symm`, `MonicCoprimeFactors.fst_map_factorPowSucc_liftFactorPow`, `irreducible_iff_card_monicCoprimeFactors`, `MonicCoprimeFactors.map_injective_of_sqZero`, `MonicCoprimeFactors.map_factorPowSucc_liftFactorPow`, `MonicCoprimeFactors.congr_rfl`, `MonicCoprimeFactors.toMonicFactors_injective`, `MonicCoprimeFactors.liftAdic_injective`, `MonicCoprimeFactors.map_surjective_of_sqZero`, `two_le_card_monicCoprimeFactors`, `MonicCoprimeFactors.congr_symm`, `MonicCoprimeFactors.map_bijective_of_isNilpotent`, `MonicCoprimeFactors.liftFactorPow_fst`, `MonicCoprimeFactors.mapEquiv_apply_snd`, `MonicCoprimeFactors.map_comp`, `MonicCoprimeFactors.congr_apply_snd`, `MonicCoprimeFactors.map_comp_map`, `MonicCoprimeFactors.liftFactorPow_snd`, `MonicCoprimeFactors.mapEquiv_apply_fst`, `MonicCoprimeFactors.map_id`, `MonicCoprimeFactors.congr_symm_apply_fst`, `MonicCoprimeFactors.mapEquiv_symm_apply_fst`, `MonicCoprimeFactors.congr_symm_apply_snd`, `MonicCoprimeFactors.mapEquiv_symm_apply_snd`, `MonicCoprimeFactors.coe_liftFactorPow`, `MonicCoprimeFactors.map_congr`, `MonicCoprimeFactors.map_bijective_of_sqZero`, `MonicCoprimeFactors.congr_apply_fst`, `MonicCoprimeFactors.map_bijective_of_isNilpotent_ker`
`MonicFactors` 📖	CompData	5 math math: `MonicCoprimeFactors.map_comp_liftAdic`, `irreducible_iff_card_monicFactors`, `MonicCoprimeFactors.toMonicFactors_injective`, `MonicCoprimeFactors.liftAdic_injective`, `two_le_card_monicFactors`
`instUniqueMonicCoprimeFactorsOfNat` 📖	CompOp	—
`instUniqueMonicFactorsOfNat` 📖	CompOp	—
`limit` 📖	CompOp	4 math math: `coeff_limit_natDegree`, `monic_limit`, `map_limit`, `natDegree_limit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_limit_natDegree` 📖	mathematical	—	`limit`	—	`IsHausdorff.eq_iff_eq` `limit.eq_1` `coeff_sum_C_mul_X_pow` `AdicCompletion.mk_ofLinearEquiv_symm_mkRing`
`coeff_sum_C_mul_X_pow` 📖	—	—	—	—	—
`degree_add_lt` 📖	—	—	—	—	—
`degree_sub_lt'` 📖	—	—	—	—	`degree_add_lt`
`degree_sum_lt'` 📖	—	—	—	—	—
`divByMonic_mem_map` 📖	—	—	—	—	—
`exists_monic_map` 📖	—	—	—	—	—
`forall_monicFactors_of_irreducible` 📖	mathematical	—	`MonicFactors.fstOne` `MonicFactors.sndOne`	—	—
`forall_monicFactors_of_natDegree_le_one` 📖	mathematical	—	`MonicFactors.fstOne` `MonicFactors.sndOne`	—	—
`irreducible_iff_card_monicCoprimeFactors` 📖	mathematical	—	`MonicCoprimeFactors`	—	`MonicCoprimeFactors.fstOne_eq_sndOne_iff` `forall_monicFactors_of_irreducible` `MonicCoprimeFactors.toMonicFactors_injective` `irreducible_of_forall_monicFactors` `MonicFactors.monic_fst` `MonicFactors.monic_snd` `MonicFactors.fst_mul_snd_eq`
`irreducible_iff_card_monicFactors` 📖	mathematical	—	`MonicFactors`	—	`MonicFactors.fstOne_eq_sndOne_iff` `forall_monicFactors_of_irreducible` `irreducible_of_forall_monicFactors`
`irreducible_map_of_irreducible_of_separable_map` 📖	—	—	—	—	`irreducible_iff_card_monicFactors` `MonicCoprimeFactors.liftAdic_injective` `irreducible_iff_card_monicCoprimeFactors` `two_le_card_monicCoprimeFactors`
`irreducible_of_forall_monicFactors` 📖	—	`MonicFactors.fstOne` `MonicFactors.sndOne`	—	—	—
`map_limit` 📖	mathematical	—	`limit`	—	`limit.eq_1` `coeff_sum_C_mul_X_pow` `AdicCompletion.mk_ofLinearEquiv_symm_mkRing`
`modByMonic_mem_map` 📖	—	—	—	—	—
`monic_limit` 📖	mathematical	—	`limit`	—	`natDegree_limit` `coeff_limit_natDegree`
`natDegree_limit` 📖	mathematical	—	`limit`	—	`natDegree_sum_lt` `coeff_limit_natDegree`
`natDegree_sum_lt` 📖	—	—	—	—	`degree_sum_lt'`
`two_le_card_monicCoprimeFactors` 📖	mathematical	—	`MonicCoprimeFactors`	—	`MonicCoprimeFactors.fstOne_eq_sndOne_iff`
`two_le_card_monicFactors` 📖	mathematical	—	`MonicFactors`	—	`MonicFactors.fstOne_eq_sndOne_iff`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_mul'` 📖	—	—	—	—	—

Polynomial.MonicCoprimeFactors

Definitions

Name	Category	Theorems
`congr` 📖	CompOp	14 math math: `congr_trans`, `coe_mapEquiv_symm`, `map_factorPowSucc_liftFactorPow`, `congr_rfl`, `congr_symm`, `map_comp`, `congr_apply_snd`, `map_comp_map`, `map_id`, `congr_symm_apply_fst`, `congr_symm_apply_snd`, `coe_liftFactorPow`, `map_congr`, `congr_apply_fst`
`fst` 📖	CompOp	20 math math: `map_fst`, `coprime_fst_snd`, `fstOne_fst_toFinsupp_support`, `fst_map_factorPowSucc_liftFactorPow`, `swap_snd`, `sndOne_fst`, `ext_iff`, `degree_fst_map`, `swap_fst`, `monic_fst`, `fstOne_fst_toFinsupp_apply`, `natDegree_fst_map`, `liftFactorPow_fst`, `toMonicFactors_fst`, `map_fst_liftAdic`, `mapEquiv_apply_fst`, `congr_symm_apply_fst`, `mapEquiv_symm_apply_fst`, `fst_mul_snd_eq`, `congr_apply_fst`
`fstOne` 📖	CompOp	4 math math: `fstOne_fst_toFinsupp_support`, `fstOne_snd`, `fstOne_fst_toFinsupp_apply`, `fstOne_eq_sndOne_iff`
`instUniqueOfSubsingleton` 📖	CompOp	—
`liftAdic` 📖	CompOp	4 math math: `map_comp_liftAdic`, `liftAdic_injective`, `map_fst_liftAdic`, `map_snd_liftAdic`
`liftFactorPow` 📖	CompOp	6 math math: `snd_map_factorPowSucc_liftFactorPow`, `fst_map_factorPowSucc_liftFactorPow`, `map_factorPowSucc_liftFactorPow`, `liftFactorPow_fst`, `liftFactorPow_snd`, `coe_liftFactorPow`
`map` 📖	CompOp	24 math math: `map_fst`, `coe_mapEquiv`, `snd_map_factorPowSucc_liftFactorPow`, `map_bijective_of_sqZero_ker`, `coe_mapEquiv_symm`, `degree_snd_map`, `fst_map_factorPowSucc_liftFactorPow`, `map_injective_of_sqZero`, `map_factorPowSucc_liftFactorPow`, `degree_fst_map`, `map_surjective_of_sqZero`, `natDegree_fst_map`, `map_bijective_of_isNilpotent`, `liftFactorPow_fst`, `natDegree_snd_map`, `map_comp`, `map_comp_map`, `liftFactorPow_snd`, `map_id`, `map_snd`, `coe_liftFactorPow`, `map_congr`, `map_bijective_of_sqZero`, `map_bijective_of_isNilpotent_ker`
`mapEquiv` 📖	CompOp	6 math math: `coe_mapEquiv`, `coe_mapEquiv_symm`, `mapEquiv_apply_snd`, `mapEquiv_apply_fst`, `mapEquiv_symm_apply_fst`, `mapEquiv_symm_apply_snd`
`snd` 📖	CompOp	20 math math: `toMonicFactors_snd`, `coprime_fst_snd`, `snd_map_factorPowSucc_liftFactorPow`, `fstOne_snd`, `degree_snd_map`, `swap_snd`, `ext_iff`, `sndOne_snd_toFinsupp_apply`, `swap_fst`, `monic_snd`, `natDegree_snd_map`, `mapEquiv_apply_snd`, `congr_apply_snd`, `liftFactorPow_snd`, `sndOne_snd_toFinsupp_support`, `map_snd`, `congr_symm_apply_snd`, `mapEquiv_symm_apply_snd`, `fst_mul_snd_eq`, `map_snd_liftAdic`
`sndOne` 📖	CompOp	4 math math: `sndOne_fst`, `sndOne_snd_toFinsupp_apply`, `fstOne_eq_sndOne_iff`, `sndOne_snd_toFinsupp_support`
`swap` 📖	CompOp	2 math math: `swap_snd`, `swap_fst`
`toMonicFactors` 📖	CompOp	4 math math: `toMonicFactors_snd`, `map_comp_liftAdic`, `toMonicFactors_injective`, `toMonicFactors_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_liftFactorPow` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `liftFactorPow` `congr` `map`	—	—
`coe_mapEquiv` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `mapEquiv` `map`	—	—
`coe_mapEquiv_symm` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `mapEquiv` `congr` `map`	—	—
`congr_apply_fst` 📖	mathematical	—	`fst` `Polynomial.MonicCoprimeFactors` `congr`	—	—
`congr_apply_snd` 📖	mathematical	—	`snd` `Polynomial.MonicCoprimeFactors` `congr`	—	—
`congr_rfl` 📖	mathematical	—	`congr` `Polynomial.MonicCoprimeFactors`	—	—
`congr_symm` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `congr`	—	—
`congr_symm_apply_fst` 📖	mathematical	—	`fst` `Polynomial.MonicCoprimeFactors` `congr`	—	—
`congr_symm_apply_snd` 📖	mathematical	—	`snd` `Polynomial.MonicCoprimeFactors` `congr`	—	—
`congr_trans` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `congr`	—	—
`coprime_fst_snd` 📖	mathematical	—	`fst` `snd`	—	—
`degree_fst_map` 📖	mathematical	—	`fst` `map`	—	`monic_fst`
`degree_snd_map` 📖	mathematical	—	`snd` `map`	—	`monic_snd`
`ext` 📖	—	`fst` `snd`	—	—	—
`ext_iff` 📖	mathematical	—	`fst` `snd`	—	`ext`
`fstOne_eq_sndOne_iff` 📖	mathematical	—	`fstOne` `sndOne`	—	—
`fstOne_fst_toFinsupp_apply` 📖	mathematical	—	`fst` `fstOne`	—	—
`fstOne_fst_toFinsupp_support` 📖	mathematical	—	`fst` `fstOne`	—	—
`fstOne_snd` 📖	mathematical	—	`snd` `fstOne`	—	—
`fst_map_factorPowSucc_liftFactorPow` 📖	mathematical	—	`fst` `map` `Polynomial.MonicCoprimeFactors` `liftFactorPow`	—	`map_factorPowSucc_liftFactorPow`
`fst_mul_snd_eq` 📖	mathematical	—	`fst` `snd`	—	—
`instIsLocalHomQuotientIdealRingHomMk` 📖	—	—	—	—	`isLocalHom_iff_one`
`instSubsingletonQuotientIdealHPowOfNat` 📖	—	—	—	—	—
`liftAdic_injective` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `Polynomial.MonicFactors` `liftAdic`	—	`map_comp_liftAdic` `toMonicFactors_injective`
`liftFactorPow_fst` 📖	mathematical	—	`fst` `Polynomial.MonicCoprimeFactors` `liftFactorPow` `map`	—	—
`liftFactorPow_snd` 📖	mathematical	—	`snd` `Polynomial.MonicCoprimeFactors` `liftFactorPow` `map`	—	—
`mapEquiv_apply_fst` 📖	mathematical	—	`fst` `Polynomial.MonicCoprimeFactors` `mapEquiv`	—	—
`mapEquiv_apply_snd` 📖	mathematical	—	`snd` `Polynomial.MonicCoprimeFactors` `mapEquiv`	—	—
`mapEquiv_symm_apply_fst` 📖	mathematical	—	`fst` `Polynomial.MonicCoprimeFactors` `mapEquiv`	—	—
`mapEquiv_symm_apply_snd` 📖	mathematical	—	`snd` `Polynomial.MonicCoprimeFactors` `mapEquiv`	—	—
`map_bijective_of_isNilpotent` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`map_comp` `map_bijective_of_sqZero_ker`
`map_bijective_of_isNilpotent_ker` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`coe_mapEquiv` `map_comp_map` `map_bijective_of_isNilpotent`
`map_bijective_of_sqZero` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`map_injective_of_sqZero` `map_surjective_of_sqZero`
`map_bijective_of_sqZero_ker` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`coe_mapEquiv` `map_comp_map` `map_bijective_of_sqZero`
`map_comp` 📖	mathematical	—	`map` `Polynomial.MonicCoprimeFactors` `congr`	—	`ext`
`map_comp_liftAdic` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `Polynomial.MonicFactors` `Polynomial.MonicFactors.map` `liftAdic` `toMonicFactors`	—	`Polynomial.MonicFactors.ext` `map_fst_liftAdic` `map_snd_liftAdic`
`map_comp_map` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map` `congr`	—	`ext`
`map_congr` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map` `congr`	—	—
`map_factorPowSucc_liftFactorPow` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map` `liftFactorPow` `congr`	—	`ext`
`map_fst` 📖	mathematical	—	`fst` `map`	—	—
`map_fst_liftAdic` 📖	mathematical	—	`Polynomial.MonicFactors.fst` `liftAdic` `fst`	—	`liftAdic.eq_1` `Polynomial.map_limit` `monic_fst` `map_fst` `liftFactorPow_fst`
`map_id` 📖	mathematical	—	`map` `Polynomial.MonicCoprimeFactors` `congr`	—	`ext`
`map_injective_of_sqZero` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`degree_snd_map`
`map_snd` 📖	mathematical	—	`snd` `map`	—	—
`map_snd_liftAdic` 📖	mathematical	—	`Polynomial.MonicFactors.snd` `liftAdic` `snd`	—	`liftAdic.eq_1` `Polynomial.map_limit` `monic_snd` `map_snd` `liftFactorPow_snd`
`map_surjective_of_sqZero` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `map`	—	`Polynomial.exists_monic_map` `IsLocalHom.of_ker_le_nilradical` `le_nilradical_of_isNilpotent` `IsCoprime.of_map` `Polynomial.modByMonic_mem_map` `Polynomial.degree_add_lt` `Polynomial.Monic.degree_mul'` `Polynomial.degree_sub_lt'` `ext`
`monic` 📖	—	—	—	—	`monic_fst` `monic_snd` `fst_mul_snd_eq`
`monic_fst` 📖	mathematical	—	`fst`	—	—
`monic_snd` 📖	mathematical	—	`snd`	—	—
`natDegree_fst_map` 📖	mathematical	—	`fst` `map`	—	`monic_fst`
`natDegree_snd_map` 📖	mathematical	—	`snd` `map`	—	`monic_snd`
`sndOne_fst` 📖	mathematical	—	`fst` `sndOne`	—	—
`sndOne_snd_toFinsupp_apply` 📖	mathematical	—	`snd` `sndOne`	—	—
`sndOne_snd_toFinsupp_support` 📖	mathematical	—	`snd` `sndOne`	—	—
`snd_map_factorPowSucc_liftFactorPow` 📖	mathematical	—	`snd` `map` `Polynomial.MonicCoprimeFactors` `liftFactorPow`	—	`map_factorPowSucc_liftFactorPow`
`swap_fst` 📖	mathematical	—	`fst` `swap` `snd`	—	—
`swap_snd` 📖	mathematical	—	`snd` `swap` `fst`	—	—
`toMonicFactors_fst` 📖	mathematical	—	`Polynomial.MonicFactors.fst` `toMonicFactors` `fst`	—	—
`toMonicFactors_injective` 📖	mathematical	—	`Polynomial.MonicCoprimeFactors` `Polynomial.MonicFactors` `toMonicFactors`	—	`ext`
`toMonicFactors_snd` 📖	mathematical	—	`Polynomial.MonicFactors.snd` `toMonicFactors` `snd`	—	—

Polynomial.MonicFactors

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	9 math math: `sndOne_fst`, `ext_iff`, `monic_fst`, `fstOne_fst_toFinsupp_apply`, `fst_mul_snd_eq`, `map_fst`, `fstOne_fst_toFinsupp_support`, `Polynomial.MonicCoprimeFactors.toMonicFactors_fst`, `Polynomial.MonicCoprimeFactors.map_fst_liftAdic`
`fstOne` 📖	CompOp	6 math math: `fstOne_fst_toFinsupp_apply`, `Polynomial.forall_monicFactors_of_natDegree_le_one`, `fstOne_eq_sndOne_iff`, `fstOne_snd`, `fstOne_fst_toFinsupp_support`, `Polynomial.forall_monicFactors_of_irreducible`
`instUniqueOfSubsingleton` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `Polynomial.MonicCoprimeFactors.map_comp_liftAdic`, `map_fst`, `map_snd`
`snd` 📖	CompOp	9 math math: `Polynomial.MonicCoprimeFactors.toMonicFactors_snd`, `ext_iff`, `monic_snd`, `sndOne_snd_toFinsupp_support`, `fst_mul_snd_eq`, `sndOne_snd_toFinsupp_apply`, `fstOne_snd`, `map_snd`, `Polynomial.MonicCoprimeFactors.map_snd_liftAdic`
`sndOne` 📖	CompOp	6 math math: `sndOne_fst`, `sndOne_snd_toFinsupp_support`, `sndOne_snd_toFinsupp_apply`, `Polynomial.forall_monicFactors_of_natDegree_le_one`, `fstOne_eq_sndOne_iff`, `Polynomial.forall_monicFactors_of_irreducible`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`fst` `snd`	—	—	—
`ext_iff` 📖	mathematical	—	`fst` `snd`	—	`ext`
`fstOne_eq_sndOne_iff` 📖	mathematical	—	`fstOne` `sndOne`	—	—
`fstOne_fst_toFinsupp_apply` 📖	mathematical	—	`fst` `fstOne`	—	—
`fstOne_fst_toFinsupp_support` 📖	mathematical	—	`fst` `fstOne`	—	—
`fstOne_snd` 📖	mathematical	—	`snd` `fstOne`	—	—
`fst_mul_snd_eq` 📖	mathematical	—	`fst` `snd`	—	—
`map_fst` 📖	mathematical	—	`fst` `map`	—	—
`map_snd` 📖	mathematical	—	`snd` `map`	—	—
`monic_fst` 📖	mathematical	—	`fst`	—	—
`monic_snd` 📖	mathematical	—	`snd`	—	—
`sndOne_fst` 📖	mathematical	—	`fst` `sndOne`	—	—
`sndOne_snd_toFinsupp_apply` 📖	mathematical	—	`snd` `sndOne`	—	—
`sndOne_snd_toFinsupp_support` 📖	mathematical	—	`snd` `sndOne`	—	—

---

← Back to Index