Sato

Statistics

Metric	Count
Definitions `M_s`, `M_s_Z`, `M_s_Z_trans`, `M_s_i`, `M_s_i_Z`, `M_s_normed`, `M_t`, `M_t_Z`, `M_t_Z_trans`, `M_t_i`, `M_t_i_Z`, `M_t_normed`, `SATO`, `SATO_action_on_R3`, `SATO_smul_R3`, `Vs`, `Vsinv`, `Vt`, `Vtinv`, `iso_forward_equiv`, `s_i_op_n`, `s_op_n`, `sato_fg3_iso`, `sato_fg3_iso_seed`, `sato_generators`, `sato_generators_ss`, `sato_s`, `sato_t`, `t_i_op_n`, `t_op_n`, `to_sato`	31
Theorems `M_s_Z_transpose_def`, `M_s_normed_is_special`, `M_s_normed_transpose_def`, `M_t_Z_transpose_def`, `M_t_normed_is_special`, `M_t_normed_transpose_def`, `SATO_smul_def`, `fnlem_s`, `fnlem_t`, `l1`, `l2`, `l3`, `l4`, `ms_def`, `msi_def`, `msinv_lem`, `msinv_lem2`, `mt_def`, `mti_def`, `mtinv_lem`, `mtinv_lem2`, `s_i_op_n_def`, `s_i_op_n_equiv`, `s_i_op_n_equiv_2`, `s_mem`, `t_i_op_n_def`, `t_i_op_n_equiv`, `t_i_op_n_equiv_2`, `t_mem`, `to_sato_is_bijective`, `to_sato_is_injective`, `to_sato_is_surjective`, `to_sato_range`	33
Total	64

(root)

Definitions

Name	Category	Theorems
`M_s` 📖	CompOp	3 math math: `msinv_lem2`, `msinv_lem`, `ms_def`
`M_s_Z` 📖	CompOp	4 math math: `M_s_Z_transpose_def`, `l1`, `ms_def`, `fnlem_s`
`M_s_Z_trans` 📖	CompOp	3 math math: `M_s_Z_transpose_def`, `M_s_normed_transpose_def`, `fnlem_s`
`M_s_i` 📖	CompOp	5 math math: `s_i_op_n_equiv_2`, `msi_def`, `s_i_op_n_equiv`, `msinv_lem2`, `msinv_lem`
`M_s_i_Z` 📖	CompOp	2 math math: `msi_def`, `l2`
`M_s_normed` 📖	CompOp	2 math math: `M_s_normed_transpose_def`, `M_s_normed_is_special`
`M_t` 📖	CompOp	3 math math: `mtinv_lem2`, `mtinv_lem`, `mt_def`
`M_t_Z` 📖	CompOp	4 math math: `fnlem_t`, `l3`, `mt_def`, `M_t_Z_transpose_def`
`M_t_Z_trans` 📖	CompOp	3 math math: `fnlem_t`, `M_t_normed_transpose_def`, `M_t_Z_transpose_def`
`M_t_i` 📖	CompOp	5 math math: `mtinv_lem2`, `t_i_op_n_equiv`, `mtinv_lem`, `mti_def`, `t_i_op_n_equiv_2`
`M_t_i_Z` 📖	CompOp	2 math math: `mti_def`, `l4`
`M_t_normed` 📖	CompOp	2 math math: `M_t_normed_transpose_def`, `M_t_normed_is_special`
`SATO` 📖	CompOp	7 math math: `to_sato_is_bijective`, `to_sato_range`, `s_mem`, `to_sato_is_injective`, `to_sato_is_surjective`, `t_mem`, `SATO_smul_def`
`SATO_action_on_R3` 📖	CompOp	—
`SATO_smul_R3` 📖	CompOp	1 math math: `SATO_smul_def`
`Vs` 📖	CompOp	—
`Vsinv` 📖	CompOp	—
`Vt` 📖	CompOp	—
`Vtinv` 📖	CompOp	—
`iso_forward_equiv` 📖	CompOp	—
`s_i_op_n` 📖	CompOp	3 math math: `s_i_op_n_equiv_2`, `s_i_op_n_def`, `s_i_op_n_equiv`
`s_op_n` 📖	CompOp	2 math math: `s_mem`, `s_i_op_n_def`
`sato_fg3_iso` 📖	CompOp	—
`sato_fg3_iso_seed` 📖	CompOp	—
`sato_generators` 📖	CompOp	—
`sato_generators_ss` 📖	CompOp	1 math math: `to_sato_range`
`sato_s` 📖	CompOp	—
`sato_t` 📖	CompOp	—
`t_i_op_n` 📖	CompOp	3 math math: `t_i_op_n_def`, `t_i_op_n_equiv`, `t_i_op_n_equiv_2`
`t_op_n` 📖	CompOp	2 math math: `t_i_op_n_def`, `t_mem`
`to_sato` 📖	CompOp	4 math math: `to_sato_is_bijective`, `to_sato_range`, `to_sato_is_injective`, `to_sato_is_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`M_s_Z_transpose_def` 📖	mathematical	—	`M_s_Z` `M_s_Z_trans`	—	—
`M_s_normed_is_special` 📖	mathematical	—	`MAT` `SO3` `M_s_normed`	—	`M_s_normed_transpose_def` `to_MAT_mul` `fnlem_s` `sevsevlem` `M_s_normed.eq_1` `M_s.eq_1` `M_s_Z.eq_1` `to_MAT.eq_1`
`M_s_normed_transpose_def` 📖	mathematical	—	`M_s_normed` `MAT` `to_MAT` `M_s_Z_trans`	—	`to_MAT_transp` `M_s_Z_transpose_def`
`M_t_Z_transpose_def` 📖	mathematical	—	`M_t_Z` `M_t_Z_trans`	—	—
`M_t_normed_is_special` 📖	mathematical	—	`MAT` `SO3` `M_t_normed`	—	`M_t_normed_transpose_def` `to_MAT_mul` `fnlem_t` `sevsevlem` `M_t_normed.eq_1` `M_t.eq_1` `M_t_Z.eq_1` `to_MAT.eq_1`
`M_t_normed_transpose_def` 📖	mathematical	—	`M_t_normed` `MAT` `to_MAT` `M_t_Z_trans`	—	`to_MAT_transp` `M_t_Z_transpose_def`
`SATO_smul_def` 📖	mathematical	—	`SO3` `SATO` `R3` `SATO_smul_R3` `to_R3`	—	—
`fnlem_s` 📖	mathematical	—	`ZMAT` `M_s_Z` `M_s_Z_trans`	—	—
`fnlem_t` 📖	mathematical	—	`ZMAT` `M_t_Z` `M_t_Z_trans`	—	—
`l1` 📖	mathematical	`Z3_raw` `Vs` `Vt` `Vtinv`	`mod7_Z` `M_s_Z`	—	—
`l2` 📖	mathematical	`Z3_raw` `Vsinv` `Vt` `Vtinv`	`mod7_Z` `M_s_i_Z`	—	—
`l3` 📖	mathematical	`Z3_raw` `Vt` `Vs` `Vsinv`	`mod7_Z` `M_t_Z`	—	—
`l4` 📖	mathematical	`Z3_raw` `Vtinv` `Vs` `Vsinv`	`mod7_Z` `M_t_i_Z`	—	—
`ms_def` 📖	mathematical	—	`M_s` `to_MAT` `M_s_Z`	—	—
`msi_def` 📖	mathematical	—	`M_s_i` `to_MAT` `M_s_i_Z`	—	—
`msinv_lem` 📖	mathematical	—	`MAT` `M_s_i` `M_s`	—	`to_MAT_mul`
`msinv_lem2` 📖	mathematical	—	`MAT` `M_s` `M_s_i`	—	`to_MAT_mul`
`mt_def` 📖	mathematical	—	`M_t` `to_MAT` `M_t_Z`	—	—
`mti_def` 📖	mathematical	—	`M_t_i` `to_MAT` `M_t_i_Z`	—	—
`mtinv_lem` 📖	mathematical	—	`MAT` `M_t_i` `M_t`	—	`to_MAT_mul`
`mtinv_lem2` 📖	mathematical	—	`MAT` `M_t` `M_t_i`	—	`to_MAT_mul`
`s_i_op_n_def` 📖	mathematical	—	`s_i_op_n` `SO3` `s_op_n`	—	—
`s_i_op_n_equiv` 📖	mathematical	—	`SO3` `s_i_op_n` `MAT` `M_s_i`	—	—
`s_i_op_n_equiv_2` 📖	mathematical	—	`SO3` `s_i_op_n` `M_s_i`	—	`s_i_op_n_equiv`
`s_mem` 📖	mathematical	—	`SO3` `SATO` `s_op_n`	—	—
`t_i_op_n_def` 📖	mathematical	—	`t_i_op_n` `SO3` `t_op_n`	—	—
`t_i_op_n_equiv` 📖	mathematical	—	`SO3` `t_i_op_n` `MAT` `M_t_i`	—	—
`t_i_op_n_equiv_2` 📖	mathematical	—	`SO3` `t_i_op_n` `M_t_i`	—	`t_i_op_n_equiv`
`t_mem` 📖	mathematical	—	`SO3` `SATO` `t_op_n`	—	—
`to_sato_is_bijective` 📖	mathematical	—	`FG2` `SO3` `SATO` `to_sato`	—	`to_sato_is_injective` `to_sato_is_surjective`
`to_sato_is_injective` 📖	mathematical	—	`FG2` `SO3` `SATO` `to_sato`	—	`wolog_zero` `drop_eq_last` `wopts` `mod_lemma_Z` `l1` `l3` `l4` `l2` `so3_invs_coe` `to_MAT_prod` `zip_lemma` `msi_def` `msinv_lem` `ms_def` `s_i_op_n_def` `s_i_op_n_equiv` `msinv_lem2` `mti_def` `mtinv_lem` `mt_def` `t_i_op_n_def` `t_i_op_n_equiv` `mtinv_lem2` `to_MAT_pow` `sev_mat_Z_mod_is_zero_lemma`
`to_sato_is_surjective` 📖	mathematical	—	`FG2` `SO3` `SATO` `to_sato`	—	`to_sato_range` `s_mem` `t_mem`
`to_sato_range` 📖	mathematical	—	`FG2` `SO3` `SATO` `to_sato` `sato_generators_ss`	—	—

---

← Back to Index