Code

associativity of ideal product#2121

Code

Open

Alizter wants to merge 12 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/associativity_of_ideal_productAlizter/HoTT:ps/rr/associativity_of_ideal_productCopy head branch name to clipboard

+568-491

Commits

Commits on Nov 18, 2024

• associativity of ideal product

  Show description for f4a9f0a
  Alizter

  committed
  f4a9f0a

• explode IdealLemmas section

  Show description for b615412
  Alizter

  committed
  b615412

• deduplicate opposite argument in ideals for ideal_produc_assoc

  Show description for f6997e2
  Alizter

  committed
  f6997e2

• change Lemma to Definition

  Show description for 5f3d2b5
  Alizter

  committed
  5f3d2b5

• fix typo

  Show description for 0c5da33
  Alizter

  committed
  0c5da33

• make leftideal_op and rightideal_op into idmap

  Show description for d225245
  Alizter

  committed
  d225245

Commits on Nov 19, 2024

• Subgroup: add subgroup_generated_subset_subgroup

  Show description for b1919ae
  jdchristensen

  committed
  b1919ae

• Ideal: use subgroup_generated_subset_subgroup and functor_subgroup_generated

  jdchristensen

  committed
  6ecda53

• Ideal: add and use ideal_product_op_triple

  jdchristensen

  committed
  f155213

• fix overzealous replacement

  Show description for 8c17c5a
  Alizter

  committed
  8c17c5a

• prove ideal_dist_r in terms of ideal_dist_l

  Show description for 5dac549
  Alizter

  committed
  5dac549

Commits on Dec 12, 2024

• Merge branch 'master' into ps/rr/associativity_of_ideal_product

  Alizter

  authored
  f80002e