OAI/RingTheory/Multiplicity/SymmetricAffine.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.IntegerWeights.SeparatelyAffine line 10
2. lemma OAI.Lech.IntegerWeights.integer_affine_of_step line 15
3. lemma OAI.Lech.IntegerWeights.separatelyAffine_of_step line 43
4. lemma OAI.Lech.IntegerWeights.affine_eq_sum_of_slopes line 57
5. lemma OAI.Lech.IntegerWeights.cons_update_zero line 78
6. theorem OAI.Lech.IntegerWeights.symmetric_affine_diagonal_constant line 85