shows "2 * (cmod (1 / complex_of_real (sqrt 2)))⇧2 = 1"
using cmod_def by (simp add: power_divide)
I suggest two_div_sqr_of_cmd_sqrt_two to stay within the name convention used for the other lemmas in the theory but shorter names are welcome.
line 461. Fact linordered_field_class.sign_simps(4) cannot be found. Proof can be replaced with
by (smt ab_semigroup_mult_class.mult_ac(1) length_greater_0_conv length_mat_to_cols_list
mat_to_cols_list_is_mat mult.Tensor.simps(1) mult.Tensor_null plus_mult_cpx plus_mult_def)
Changed one metis proof in Deutsch_Joza by one that requires less time.
Theory No_Cloning line 193. Assumptions have [simp] attributes. Do they need a name too? I am not sure what the [simp] does here.
Added Measurement to ROOT since all theory files of the submission must be contained in at least one session.
Last updated: Dec 07 2023 at 16:21 UTC