Skip to content

Commit

Permalink
Deploying to gh-pages from @ d121fbb 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@themathqueen
themathqueen committed Feb 8, 2024
1 parent 39a95dc commit 6a5dcaf
Show file tree
Hide file tree
Showing 1,421 changed files with 4,148 additions and 4,152 deletions.
Binary file modified export_db.json.gz
View file
Binary file not shown.
4 changes: 2 additions & 2 deletions find/D_in/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L474");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L474">D_in source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L474");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L474">D_in source</a></noscript>
4 changes: 2 additions & 2 deletions find/D_in_Schur_product_eq_ir_refl/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L659");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L659">D_in_Schur_product_eq_ir_refl source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L659");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L659">D_in_Schur_product_eq_ir_refl source</a></noscript>
4 changes: 2 additions & 2 deletions find/D_in_apply/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L492");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L492">D_in_apply source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L492");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L492">D_in_apply source</a></noscript>
4 changes: 2 additions & 2 deletions find/D_out/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L481");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L481">D_out source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L481");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L481">D_out source</a></noscript>
4 changes: 2 additions & 2 deletions find/D_out_Schur_product_eq_ir_refl'/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L683");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L683">D_out_Schur_product_eq_ir_refl' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L683");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L683">D_out_Schur_product_eq_ir_refl' source</a></noscript>
4 changes: 2 additions & 2 deletions find/D_out_apply/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L500");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L500">D_out_apply source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L500");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L500">D_out_apply source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.adjoint/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L718");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L718">Psi.adjoint source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L718");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L718">Psi.adjoint source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.one/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/qam_A.lean#L136");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/qam_A.lean#L136">Psi.one source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/qam_A.lean#L136");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/qam_A.lean#L136">Psi.one source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.real/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L950");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L950">Psi.real source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L950");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L950">Psi.real source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.refl_idempotent/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L674");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L674">Psi.refl_idempotent source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L674");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L674">Psi.refl_idempotent source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.symmetric'/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L655");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L655">Psi.symmetric' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L655");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L655">Psi.symmetric' source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi.symmetric/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L632");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/nontracial.lean#L632">Psi.symmetric source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L632");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/nontracial.lean#L632">Psi.symmetric source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi_apply_complete_graph/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/to_projections.lean#L471");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/to_projections.lean#L471">Psi_apply_complete_graph source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/to_projections.lean#L471");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/to_projections.lean#L471">Psi_apply_complete_graph source</a></noscript>
4 changes: 2 additions & 2 deletions find/Psi_inv_0_0_mul_adjoint_eq_lmul/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L199");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/quantum_graph/mess.lean#L199">Psi_inv_0_0_mul_adjoint_eq_lmul source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L199");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/quantum_graph/mess.lean#L199">Psi_inv_0_0_mul_adjoint_eq_lmul source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sq_add_sq_abs_sq_add_abs_sq_iff''/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L112");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L112">abs_of_sq_add_sq_abs_sq_add_abs_sq_iff'' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L112");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L112">abs_of_sq_add_sq_abs_sq_add_abs_sq_iff'' source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sq_add_sq_abs_sq_add_abs_sq_iff'/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L86");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L86">abs_of_sq_add_sq_abs_sq_add_abs_sq_iff' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L86");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L86">abs_of_sq_add_sq_abs_sq_add_abs_sq_iff' source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sq_add_sq_eq_abs_sq_add_abs_sq_iff/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L68");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L68">abs_of_sq_add_sq_eq_abs_sq_add_abs_sq_iff source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L68");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L68">abs_of_sq_add_sq_eq_abs_sq_add_abs_sq_iff source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sum_sq_eq_sum_abs_sq_iff''/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L155");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L155">abs_of_sum_sq_eq_sum_abs_sq_iff'' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L155");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L155">abs_of_sum_sq_eq_sum_abs_sq_iff'' source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sum_sq_eq_sum_abs_sq_iff'/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L103");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L103">abs_of_sum_sq_eq_sum_abs_sq_iff' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L103");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L103">abs_of_sum_sq_eq_sum_abs_sq_iff' source</a></noscript>
4 changes: 2 additions & 2 deletions find/abs_of_sum_sq_eq_sum_abs_sq_iff/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L21");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/complex.lean#L21">abs_of_sum_sq_eq_sum_abs_sq_iff source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L21");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/complex.lean#L21">abs_of_sum_sq_eq_sum_abs_sq_iff source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_equiv.comp_inj/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L17");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L17">alg_equiv.comp_inj source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L17");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L17">alg_equiv.comp_inj source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_equiv.eq_apply_iff_symm_eq/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L143");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L143">alg_equiv.eq_apply_iff_symm_eq source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L143");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L143">alg_equiv.eq_apply_iff_symm_eq source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_equiv.inj_comp/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L26");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L26">alg_equiv.inj_comp source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L26");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L26">alg_equiv.inj_comp source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_equiv.map_eq_zero_iff/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L109");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L109">alg_equiv.map_eq_zero_iff source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L109");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L109">alg_equiv.map_eq_zero_iff source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_equiv.one_to_linear_map/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L104");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/preq/star_alg_equiv.lean#L104">alg_equiv.one_to_linear_map source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L104");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/preq/star_alg_equiv.lean#L104">alg_equiv.one_to_linear_map source</a></noscript>
4 changes: 2 additions & 2 deletions find/alg_hom.commute_map_mul'/src/index.html
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
<script src="https://themathqueen.github.io/monlib/add_commit.js"></script>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/linear_algebra/my_tensor_product.lean#L265");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/0a1edf417575e1c326e4583558c41ee973483f64/src/linear_algebra/my_tensor_product.lean#L265">alg_hom.commute_map_mul' source</a></noscript>
<script>redirectTo("https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/linear_algebra/my_tensor_product.lean#L265");</script>
<noscript><a href="https://github.com/themathqueen/monlib/blob/d121fbb0e2b5d3ac17c2b8344cec464e5cf90245/src/linear_algebra/my_tensor_product.lean#L265">alg_hom.commute_map_mul' source</a></noscript>
Loading

0 comments on commit 6a5dcaf

Please sign in to comment.