Commit 2024-02-26 22:59 f633abad

View on Github →

feat: fractional polymorphisms for VCSP (#7894)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem Fin.prod_univ_two'

Modified Mathlib/Combinatorics/Optimization/ValuedCSP.lean

added def FractionalOperation.IsFractionalPolymorphismFor

added def FractionalOperation.IsSymmetric

added def FractionalOperation.IsSymmetricFractionalPolymorphismFor

added theorem FractionalOperation.IsValid.contains

added def FractionalOperation.IsValid

added def FractionalOperation.size

added def FractionalOperation.tt

added def Function.AdmitsFractional

added theorem Function.HasMaxCutProperty.forbids_commutativeFractionalPolymorphism

added def Function.HasMaxCutProperty

added theorem Function.HasMaxCutPropertyAt.rows_lt_aux

added def Function.HasMaxCutPropertyAt

Modified Mathlib/Data/Fin/VecNotation.lean

added theorem Matrix.const_fin1_eq