SatoUtils

📁 Source: BanachTarski/SatoUtils.lean

Statistics

Metric	Count
Definitions `S_f`, `TailPred_f`, `Z3_raw`, `ZMAT`, `all_s_f`, `all_sinv_f`, `first_is_sinv_f`, `lSet_type_f`, `last_is_sigma_f`, `leading_others_as_nat_f`, `leading_s_as_nat_f`, `max_fin_f`, `mod7_Z`, `n_trail_sinv_f`, `sev_mat`, `sev_mat_Z`, `seventh_mat`, `to_MAT`, `trailing_as_nat_f`	19
Theorems `TP_holds_of_zero_f`, `all_sinv_equiv`, `collapse_replics_1`, `collapse_replics_2`, `diagonal_const_comm`, `drop_eq_last`, `if_not_all_init_s_w`, `if_not_all_sinv_w`, `inv7lemma`, `isReduced_of_invRev_of_isReduced`, `isReduced_of_replicate`, `isreduced_of_append_of_reduced_mismatching_boundary`, `isreduced_of_drop_of_reduced`, `isreduced_of_take_of_reduced`, `leading_trailing`, `mod7_Z_additive`, `mod7_Z_idempotent`, `mod_lemma_Z`, `ne_S_f`, `reduce_invRev_right_cancel`, `sev_mat_Z_mod_is_zero_lemma`, `sevsevlem`, `to_MAT_inj`, `to_MAT_mul`, `to_MAT_pow`, `to_MAT_prod`, `to_MAT_transp`, `wolog_zero`, `zip_lemma`	29
Total	48

(root)

Definitions

Name	Category	Theorems
`S_f` 📖	CompOp	1 math math: `ne_S_f`
`TailPred_f` 📖	CompOp	1 bridge bridge: `TP_holds_of_zero_f`
`Z3_raw` 📖	CompOp	2 math math: `mod7_Z_additive`, `sev_mat_Z_mod_is_zero_lemma`
`ZMAT` 📖	CompOp	6 math math: `fnlem_t`, `to_MAT_pow`, `to_MAT_mul`, `to_MAT_prod`, `to_MAT_inj`, `fnlem_s`
`all_s_f` 📖	MathDef	—
`all_sinv_f` 📖	MathDef	—
`first_is_sinv_f` 📖	MathDef	—
`lSet_type_f` 📖	CompOp	1 math math: `ne_S_f`
`last_is_sigma_f` 📖	MathDef	—
`leading_others_as_nat_f` 📖	CompOp	—
`leading_s_as_nat_f` 📖	CompOp	2 math math: `if_not_all_init_s_w`, `leading_trailing`
`max_fin_f` 📖	CompOp	—
`mod7_Z` 📖	CompOp	8 math math: `mod7_Z_additive`, `mod_lemma_Z`, `l3`, `l1`, `mod7_Z_idempotent`, `l4`, `sev_mat_Z_mod_is_zero_lemma`, `l2`
`n_trail_sinv_f` 📖	CompOp	—
`sev_mat` 📖	CompOp	1 math math: `inv7lemma`
`sev_mat_Z` 📖	CompOp	1 math math: `sev_mat_Z_mod_is_zero_lemma`
`seventh_mat` 📖	CompOp	1 math math: `inv7lemma`
`to_MAT` 📖	CompOp	11 math math: `to_MAT_transp`, `msi_def`, `M_s_normed_transpose_def`, `to_MAT_pow`, `to_MAT_mul`, `M_t_normed_transpose_def`, `to_MAT_prod`, `mti_def`, `ms_def`, `to_MAT_inj`, `mt_def`
`trailing_as_nat_f` 📖	CompOp	2 math math: `if_not_all_sinv_w`, `leading_trailing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`TP_holds_of_zero_f` 📖	bridging (complete)	—	`TailPred_f`	`TailPred_f`	—
`all_sinv_equiv` 📖	mathematical	`all_sinv_f`	`chartype`	—	`ne_S_f`
`collapse_replics_1` 📖	mathematical	—	`σchar`	—	`reduce_invRev_right_cancel`
`collapse_replics_2` 📖	mathematical	—	`σchar`	—	`collapse_replics_1`
`diagonal_const_comm` 📖	mathematical	—	`MAT`	—	—
`drop_eq_last` 📖	—	—	—	—	—
`if_not_all_init_s_w` 📖	mathematical	`all_s_f` `first_is_sinv_f`	`chartype` `leading_s_as_nat_f`	—	`all_sinv_equiv` `if_not_all_sinv_w` `leading_trailing` `isReduced_of_invRev_of_isReduced`
`if_not_all_sinv_w` 📖	mathematical	`all_sinv_f` `last_is_sigma_f`	`chartype` `trailing_as_nat_f`	—	`ne_S_f` `isreduced_of_take_of_reduced` `wopts`
`inv7lemma` 📖	mathematical	—	`MAT` `sev_mat` `seventh_mat`	—	—
`isReduced_of_invRev_of_isReduced` 📖	—	—	—	—	—
`isReduced_of_replicate` 📖	—	—	—	—	—
`isreduced_of_append_of_reduced_mismatching_boundary` 📖	—	—	—	—	—
`isreduced_of_drop_of_reduced` 📖	—	—	—	—	—
`isreduced_of_take_of_reduced` 📖	—	—	—	—	—
`leading_trailing` 📖	mathematical	—	`trailing_as_nat_f` `leading_s_as_nat_f`	—	—
`mod7_Z_additive` 📖	mathematical	—	`mod7_Z` `Z3_raw`	—	—
`mod7_Z_idempotent` 📖	mathematical	—	`mod7_Z`	—	—
`mod_lemma_Z` 📖	mathematical	—	`mod7_Z`	—	`mod7_Z_additive` `mod7_Z_idempotent`
`ne_S_f` 📖	mathematical	—	`lSet_type_f` `S_f`	—	`TP_holds_of_zero_f`
`reduce_invRev_right_cancel` 📖	mathematical	—	`chartype`	—	—
`sev_mat_Z_mod_is_zero_lemma` 📖	mathematical	—	`mod7_Z` `sev_mat_Z` `Z3_raw`	—	—
`sevsevlem` 📖	—	—	—	—	—
`to_MAT_inj` 📖	mathematical	—	`ZMAT` `MAT` `to_MAT`	—	—
`to_MAT_mul` 📖	mathematical	—	`to_MAT` `ZMAT` `MAT`	—	—
`to_MAT_pow` 📖	mathematical	—	`to_MAT` `ZMAT` `MAT`	—	`to_MAT_prod`
`to_MAT_prod` 📖	mathematical	—	`to_MAT` `ZMAT` `MAT`	—	`to_MAT_mul`
`to_MAT_transp` 📖	mathematical	—	`to_MAT`	—	—
`wolog_zero` 📖	—	`FG2`	—	—	`ne_S_f` `if_not_all_sinv_w` `collapse_replics_2` `isreduced_of_append_of_reduced_mismatching_boundary` `if_not_all_init_s_w` `σ_def` `collapse_replics_1` `isReduced_of_replicate`
`zip_lemma` 📖	—	`MAT`	—	—	`diagonal_const_comm`

---

← Back to Index