FixedPointLemma

📁 Source: BanachTarski/FixedPointLemma.lean

Statistics

Metric	Count
Definitions `C3`, `CONJ`, `K`, `as_complex`, `cpoly`, `g_end`, `g_end_raw`, `kermap`, `kermap_raw`, `ofLp_linear`, `to_R3_linear`	11
Theorems `K_id`, `cast_root_mult1`, `charpoly_deg_3`, `charpoly_natdeg_3`, `conj_mul_roots`, `conj_roots`, `conj_roots_2`, `conj_roots_3`, `conj_roots_4`, `cpoly_coef_real`, `det_as_prod`, `dim_ker`, `eig_norms`, `fixed_lemma`, `flem`, `flem2`, `idlem`, `mapMatrix_is_map`, `num_roots_eq_3`, `num_roots_eq_deg`, `same_char`, `same_char_0`, `same_mult`, `spec_lem`, `tight_space_lemma`, `tight_space_lemma_2`	26
Total	37

(root)

Definitions

Name	Category	Theorems
`C3` 📖	CompOp	—
`CONJ` 📖	CompOp	4 math math: `conj_mul_roots`, `conj_roots_2`, `conj_roots_3`, `conj_roots`
`K` 📖	CompOp	2 math math: `K_id`, `dim_ker`
`as_complex` 📖	CompOp	—
`cpoly` 📖	CompOp	10 math math: `spec_lem`, `same_char`, `conj_roots_3`, `num_roots_eq_3`, `cpoly_coef_real`, `conj_roots`, `det_as_prod`, `charpoly_natdeg_3`, `num_roots_eq_deg`, `charpoly_deg_3`
`g_end` 📖	CompOp	4 math math: `same_char`, `same_char_0`, `K_id`, `same_mult`
`g_end_raw` 📖	CompOp	—
`kermap` 📖	CompOp	—
`kermap_raw` 📖	CompOp	—
`ofLp_linear` 📖	CompOp	—
`to_R3_linear` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`K_id` 📖	mathematical	—	`K` `R3` `g_end`	—	—
`cast_root_mult1` 📖	mathematical	—	`SO3`	—	—
`charpoly_deg_3` 📖	mathematical	—	`cpoly`	—	—
`charpoly_natdeg_3` 📖	mathematical	—	`cpoly`	—	—
`conj_mul_roots` 📖	mathematical	`cpoly`	`CONJ`	—	`eig_norms`
`conj_roots` 📖	mathematical	—	`cpoly` `CONJ`	—	`cpoly_coef_real` `charpoly_natdeg_3` `num_roots_eq_deg`
`conj_roots_2` 📖	mathematical	`cpoly`	`CONJ`	—	`conj_roots`
`conj_roots_3` 📖	mathematical	—	`cpoly` `CONJ`	—	`conj_roots`
`conj_roots_4` 📖	—	`cpoly`	—	—	`conj_roots_3` `flem2` `num_roots_eq_3`
`cpoly_coef_real` 📖	mathematical	—	`cpoly`	—	`same_char`
`det_as_prod` 📖	mathematical	—	`cpoly`	—	—
`dim_ker` 📖	mathematical	—	`R3` `K`	—	`K_id` `spec_lem` `same_mult` `same_char`
`eig_norms` 📖	—	`cpoly`	—	—	—
`fixed_lemma` 📖	mathematical	—	`R3` `S2` `SO3`	—	`dim_ker` `SO3_smul_def` `normed_in_S2`
`flem` 📖	—	`cpoly` `CONJ`	—	—	`eig_norms`
`flem2` 📖	—	`cpoly`	—	—	`flem`
`idlem` 📖	mathematical	`cpoly`	`SO3`	—	—
`mapMatrix_is_map` 📖	mathematical	—	`SO3`	—	—
`num_roots_eq_3` 📖	mathematical	—	`cpoly`	—	`num_roots_eq_deg` `charpoly_natdeg_3`
`num_roots_eq_deg` 📖	mathematical	—	`cpoly`	—	—
`same_char` 📖	mathematical	—	`R3` `g_end` `cpoly`	—	`mapMatrix_is_map` `same_char_0`
`same_char_0` 📖	mathematical	—	`R3` `g_end` `SO3`	—	—
`same_mult` 📖	mathematical	—	`R3` `g_end`	—	`same_char` `mapMatrix_is_map` `same_char_0` `cast_root_mult1`
`spec_lem` 📖	mathematical	—	`cpoly`	—	`num_roots_eq_3` `idlem` `det_as_prod` `tight_space_lemma_2` `tight_space_lemma` `flem2` `conj_roots_2` `conj_mul_roots` `conj_roots_4` `conj_roots_3`
`tight_space_lemma` 📖	—	`cpoly`	—	—	`flem2` `conj_roots_2` `num_roots_eq_3`
`tight_space_lemma_2` 📖	—	`cpoly`	—	—	`tight_space_lemma` `num_roots_eq_3`

---

← Back to Index