Commit 2024-04-18 06:50 eb70190a

View on Github →

feat: lemmas about Array.extract (#11621)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Array/ExtractLemmas.lean

added theorem Array.extract_append_left

added theorem Array.extract_append_right

added theorem Array.extract_eq_nil_of_start_eq_end

added theorem Array.extract_eq_of_size_le_end

added theorem Array.extract_extract