Skip to content

Commit c23cf27

Browse files
adomaniTOMILO87
authored andcommitted
chore: remove whitespace (#25363)
Found by #24465,
1 parent c1e873b commit c23cf27

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/RingTheory/Radical.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ lemma primeFactors_val_eq_normalizedFactors (ha : IsRadical a) :
125125
exact normalizedFactors_nodup ha
126126

127127
-- Note that the non-zero assumptions are necessary here.
128-
theorem primeFactors_mul_eq_union [DecidableEq M] (ha : a ≠ 0) (hb : b ≠ 0) :
128+
theorem primeFactors_mul_eq_union [DecidableEq M] (ha : a ≠ 0) (hb : b ≠ 0) :
129129
primeFactors (a * b) = primeFactors a ∪ primeFactors b := by
130130
ext p
131131
simp [mem_normalizedFactors_iff', mem_primeFactors, ha, hb]

0 commit comments

Comments
 (0)