Hanna Lachnitt (Oct 07 2020 at 20:09): Hanna Lachnitt (Oct 07 2020 at 20:09):Basics.thy:
lemma [simp]:
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.
Hanna Lachnitt (Oct 07 2020 at 21:28):Tensor.thy:
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)
Hanna Lachnitt (Oct 09 2020 at 20:46):Changed one metis proof in Deutsch_Joza by one that requires less time.
Hanna Lachnitt (Oct 09 2020 at 21:01):Theory No_Cloning line 193. Assumptions have [simp] attributes. Do they need a name too? I am not sure what the [simp] does here.
Hanna Lachnitt (Oct 16 2020 at 18:48):Added Measurement to ROOT since all theory files of the submission must be contained in at least one session.
Last updated: Nov 21 2024 at 08:25 UTC